Menu
▾
▴
golok-commit — Committers List
You can subscribe to this list here.
| 2010 |
Jan
|
Feb
(8) |
Mar
(17) |
Apr
(1) |
May
|
Jun
(3) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|---|
|
From: <sr...@us...> - 2010-06-18 16:49:47
|
Revision: 29
http://golok.svn.sourceforge.net/golok/?rev=29&view=rev
Author: sralmai
Date: 2010-06-18 16:49:41 +0000 (Fri, 18 Jun 2010)
Log Message:
-----------
[BUGFIX]: finished solving bug from previous release, added script for packaging binaries
Modified Paths:
--------------
trunk/datatypes.scm
trunk/examples/dme-mult.amf
trunk/find-k.scm
trunk/model-builder.scm
Added Paths:
-----------
trunk/package.sh
Modified: trunk/datatypes.scm
===================================================================
--- trunk/datatypes.scm 2010-06-15 22:12:17 UTC (rev 28)
+++ trunk/datatypes.scm 2010-06-18 16:49:41 UTC (rev 29)
@@ -9,6 +9,9 @@
#lang scheme
+;; for docs
+(require scribble/base scribble/srcdoc)
+
(provide
; behavioral automaton
(struct-out automaton)
@@ -34,7 +37,7 @@
ot_pt2zi
;; utility functions
- display-ln
+ display-ln
list-of-lists->list
los->string
lostrings->string
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-06-15 22:12:17 UTC (rev 28)
+++ trunk/examples/dme-mult.amf 2010-06-18 16:49:41 UTC (rev 29)
@@ -5,17 +5,16 @@
# "normal" nodes and pass nodes (as in "Automating Cut-off..")
#
#
-process critical {
-ENTER: [ Idle, token2 ] -> [ Cs , in ]
-LEAVE: [ Cs , in ] -> [ Idle , token ]
-
-}
-
process forward {
IDLE: [ Idle, token ] -> [ Idle, token2 ]
SND: [ Start, epsilon ] -> [ Idle, token2 ]
}
+process critical {
+ENTER: [ Idle, token2 ] -> [ Cs , in ]
+LEAVE: [ Cs , in ] -> [ Idle , token ]
+}
+
topology {
connectivity {
critical 0 -- forward 0
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-06-15 22:12:17 UTC (rev 28)
+++ trunk/find-k.scm 2010-06-18 16:49:41 UTC (rev 29)
@@ -194,7 +194,7 @@
; (void))
(dump-sys
(model2dot (find-solution (item-index (automaton-proc-type x) processes) x)
- (string-append output-directory "/" (symbol->string proc-type) "-sys.dot") npp))
+ (build-path output-directory (string-append (symbol->string proc-type) "-sys.dot")) npp))
(#t
(find-solution (item-index (automaton-proc-type x) processes) x)))))
eps-auts))
@@ -221,7 +221,7 @@
[mask (remove name names)])
(let-values ([(tt oneE-builder) (build-oneEmodel-builder prot)])
(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))])
+ (build-path output-directory (string-append (symbol->string name) "-1e.dot")) #:show-buf #f) (void))])
(let-values ([(soln data) (search prot k name dfs start-aut
#:pruning pruning
#:npp npp
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-06-15 22:12:17 UTC (rev 28)
+++ trunk/model-builder.scm 2010-06-18 16:49:41 UTC (rev 29)
@@ -658,7 +658,6 @@
[to-id (get-id (state->representative (todo->next-state z) sp) db)])
(add-trans-to-set! (todo-state z) (todo->label to-id z) db)))
(filter (lambda (g) (and (hash-has-key? db (state->representative (todo->next-state g) sp)) (hash-has-key? db (state->representative (todo-state g) sp)))) todos)))))
-
(let ([vect (make-vector (hash-count db))])
(begin
(hash-for-each db (lambda (x y)
Added: trunk/package.sh
===================================================================
--- trunk/package.sh (rev 0)
+++ trunk/package.sh 2010-06-18 16:49:41 UTC (rev 29)
@@ -0,0 +1,24 @@
+#!/bin/bash
+
+# pack up for a binary distribution
+
+NAME=""
+
+if [[ -z $1 ]]
+then
+ NAME="support";
+else
+NAME=golok-bin-v$1;
+fi
+
+make
+
+mzc --exe-dir $NAME golok
+
+mkdir $NAME/examples
+cp examples/*.amf $NAME/examples/
+cp README $NAME/
+
+tar cjvf $NAME.tar.bz2 $NAME
+
+rm -rf $NAME
\ No newline at end of file
Property changes on: trunk/package.sh
___________________________________________________________________
Added: svn:executable
+ *
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-06-15 22:12:23
|
Revision: 28
http://golok.svn.sourceforge.net/golok/?rev=28&view=rev
Author: sralmai
Date: 2010-06-15 22:12:17 +0000 (Tue, 15 Jun 2010)
Log Message:
-----------
[BUGFIX]: path mangling problem for sytem configuration file ouptut fixed
Modified Paths:
--------------
trunk/find-k.scm
trunk/golok.scm
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-06-14 01:39:43 UTC (rev 27)
+++ trunk/find-k.scm 2010-06-15 22:12:17 UTC (rev 28)
@@ -130,16 +130,17 @@
; sanity check on file (mostly to prevent pathlist-closure from being called on a directory)
(if (not (file-exists? filename)) (raise-user-error filename " not found!")
; save the path of filename
- (let ([cl (pathlist-closure (list filename))])
+ (let ([cl (path->complete-path (string->path filename))])
+ (let-values ([(amf-dir amf-file dir?) (split-path cl)])
(begin
- (set! amf-directory (path->string (list-ref cl (- (length cl) 2))))
+ (set! amf-directory amf-dir)
(if (not output-directory) (set! output-directory amf-directory) (void)))
(set! prot (parse-amf-file filename))
(set! base-name (parse-filename filename))
(set! start-time (current-seconds))
; k is current system instance
- (set! k (protocol-kernel prot))))))
+ (set! k (protocol-kernel prot)))))))
(define parse-filename
(lambda (fn)
@@ -202,7 +203,8 @@
(define dump-solution
(lambda ()
- (let ([output-name (string-append output-directory "/" (strip-folder base-name) "-cutoff.topo")])
+ (let ([output-name (simplify-path (build-path output-directory
+ (string-append (strip-folder base-name) "-cutoff.topo")))])
(begin
(topology->file k output-name)
(display-ln "The cut-off system has " (topology->string k) " processes.")
@@ -316,13 +318,5 @@
; (string?) -> (string?)
(define strip-folder
(lambda (x)
- (let ([rev-chars (reverse (string->list x))])
- (list->string (reverse (strip-folder-rec rev-chars))))))
-
-; (list-of char?) -> (list-of char?)
-(define strip-folder-rec
- (lambda (x)
- (cond
- ((null? x) '())
- ((or (eq? (car x) #\/) (eq? (car x) #\\)) '())
- (#t (cons (car x) (strip-folder-rec (cdr x)))))))
+ (let-values ([(dir-path file dir?) (split-path x)])
+ (path->string file))))
Modified: trunk/golok.scm
===================================================================
--- trunk/golok.scm 2010-06-14 01:39:43 UTC (rev 27)
+++ trunk/golok.scm 2010-06-15 22:12:17 UTC (rev 28)
@@ -8,7 +8,7 @@
(require scheme/cmdline)
;; version header -- should be in form vx.y.z(-tag)
- (define version "v1.2.0")
+ (define version "v1.2.1")
; parsed values of command line arguments
; currently size 11
@@ -44,7 +44,7 @@
(define dump #f)
; output directory
- (define output-directory "output")
+ (define output-directory #f)
; fast forward (skip) searching n levels of bfs tree
; TODO: not implemented
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-06-14 01:39:49
|
Revision: 27
http://golok.svn.sourceforge.net/golok/?rev=27&view=rev
Author: sralmai
Date: 2010-06-14 01:39:43 +0000 (Mon, 14 Jun 2010)
Log Message:
-----------
[CLEANUP]: changed dme and dme-mult to begin with 2 of each process type
Modified Paths:
--------------
trunk/examples/dme-mult.amf
trunk/examples/dme.amf
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-04-19 15:34:15 UTC (rev 26)
+++ trunk/examples/dme-mult.amf 2010-06-14 01:39:43 UTC (rev 27)
@@ -19,7 +19,9 @@
topology {
connectivity {
critical 0 -- forward 0
- forward 0 -- critical 0
+ forward 0 -- critical 1
+ critical 1 -- forward 1
+ forward 1 -- critical 0
}
# insert two new elements (a forward and a critical) into the ring
Modified: trunk/examples/dme.amf
===================================================================
--- trunk/examples/dme.amf 2010-04-19 15:34:15 UTC (rev 26)
+++ trunk/examples/dme.amf 2010-06-14 01:39:43 UTC (rev 27)
@@ -15,7 +15,8 @@
topology {
connectivity {
- node 0 -- node 0
+ node 0 -- node 1
+ node 1 -- node 0
}
additionrule plain-add {
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-04-19 15:34:22
|
Revision: 26
http://golok.svn.sourceforge.net/golok/?rev=26&view=rev
Author: sralmai
Date: 2010-04-19 15:34:15 +0000 (Mon, 19 Apr 2010)
Log Message:
-----------
[BUGFIX (ID:2976528)]: undocumented coupling removed
Modified Paths:
--------------
trunk/Makefile
trunk/datatypes.scm
trunk/parser.scm
trunk/topo-datatypes.scm
Modified: trunk/Makefile
===================================================================
--- trunk/Makefile 2010-03-25 17:52:38 UTC (rev 25)
+++ trunk/Makefile 2010-04-19 15:34:15 UTC (rev 26)
@@ -1,6 +1,9 @@
golok: lookup-table.scm datatypes.scm model-builder.scm search.scm golok.scm find-k.scm parser.scm topo-datatypes.scm
mzc --exe golok golok.scm
+test:
+ ./run-all.sh
+
render:
output/render.sh
Modified: trunk/datatypes.scm
===================================================================
--- trunk/datatypes.scm 2010-03-25 17:52:38 UTC (rev 25)
+++ trunk/datatypes.scm 2010-04-19 15:34:15 UTC (rev 26)
@@ -41,6 +41,7 @@
cons-to-vec
append-to-vec
cons-to-hash
+ symbol<?
state->process
@@ -212,3 +213,11 @@
((null? ls) -1)
((equal? item (car ls)) index)
(#t (item-index-rec item (add1 index) (cdr ls))))))
+
+
+;;
+;; wrapper for string<? on symbols
+;;
+(define (symbol<? x y)
+ (string<? (symbol->string x) (symbol->string y)))
+
Modified: trunk/parser.scm
===================================================================
--- trunk/parser.scm 2010-03-25 17:52:38 UTC (rev 25)
+++ trunk/parser.scm 2010-04-19 15:34:15 UTC (rev 26)
@@ -281,7 +281,10 @@
; first do some quick sanity checks
(if (zero? (length p_processes)) (raise-user-error 'PARSE "no processes defined!") (void))
(if (zero? (length p_add-rules)) (raise-user-error 'PARSE "no addition rules defined!") (void))
- (let* ([procs (map p_proc2proc p_processes)]
+ (let* ([procs (sort (map p_proc2proc p_processes)
+ (lambda (x y)
+ (string<? (symbol->string (process-name x))
+ (symbol->string (process-name y)))))]
[add-rules (map parse-rule p_add-rules)]
[the-topo (parse-topo p_transitions)]
[names (map process-name procs)]
@@ -554,7 +557,7 @@
(define (create-kernel filename p_links)
(let* ([links (map parse_link p_links)]
[counts (count-links links)])
- (make-topology filename counts links)))
+ (make-topology filename (sort counts (lambda (x y) (symbol<? (car x) (car y)))) links)))
;;
;; (list-of link?
Modified: trunk/topo-datatypes.scm
===================================================================
--- trunk/topo-datatypes.scm 2010-03-25 17:52:38 UTC (rev 25)
+++ trunk/topo-datatypes.scm 2010-04-19 15:34:15 UTC (rev 26)
@@ -208,7 +208,7 @@
; (list-of-links result-from-verify-and-build-offsets) -> listing of each process, process type, and input id
(define build-model
- (lambda (lol offset-table)
+ (lambda (lol offset-table)
(let* ([size (ot_size offset-table)]
[vect (make-vector size (list))]
[dummy (for-each (lambda (x) (add-link x vect offset-table)) lol)])
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-03-25 17:52:44
|
Revision: 25
http://golok.svn.sourceforge.net/golok/?rev=25&view=rev
Author: sralmai
Date: 2010-03-25 17:52:38 +0000 (Thu, 25 Mar 2010)
Log Message:
-----------
[RELEASE PACKAGING]: version 1.2 candidate #2
Modified Paths:
--------------
trunk/examples/SpinLock-mult.amf
trunk/examples/SpinLock.amf
trunk/examples/dme-mult.amf
trunk/examples/dme.amf
trunk/examples/dpp.amf
trunk/examples/lr-dpp.amf
trunk/examples/producer-consumer.amf
trunk/parser.scm
Removed Paths:
-------------
trunk/examples/SpinLock-mult.topo
trunk/examples/SpinLock.topo
trunk/examples/dme-mult.topo
trunk/examples/dme.topo
trunk/examples/dpp.topo
trunk/examples/lr-dpp-11.topo
trunk/examples/lr-dpp-22.topo
trunk/examples/lr-dpp-33.topo
trunk/examples/lr-dpp-66.topo
trunk/examples/lr-dpp-88.topo
trunk/examples/lr-dpp.topo
trunk/examples/milners.topo
trunk/examples/producer-consumer.topo
Modified: trunk/examples/SpinLock-mult.amf
===================================================================
--- trunk/examples/SpinLock-mult.amf 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/SpinLock-mult.amf 2010-03-25 17:52:38 UTC (rev 25)
@@ -55,5 +55,5 @@
}
}
-initial-config {
+initialconfig {
}
Deleted: trunk/examples/SpinLock-mult.topo
===================================================================
--- trunk/examples/SpinLock-mult.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/SpinLock-mult.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,12 +0,0 @@
-model: SpinLock.amf
-
-counts:
-thread 2
-object 2
-
-links:
-
-thread 0 -- object 0
-thread 0 -- object 1
-thread 1 -- object 0
-thread 1 -- object 1
Modified: trunk/examples/SpinLock.amf
===================================================================
--- trunk/examples/SpinLock.amf 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/SpinLock.amf 2010-03-25 17:52:38 UTC (rev 25)
@@ -45,5 +45,5 @@
}
}
-initial-config {
+initialconfig {
}
Deleted: trunk/examples/SpinLock.topo
===================================================================
--- trunk/examples/SpinLock.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/SpinLock.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,10 +0,0 @@
-model: SpinLock.amf
-
-counts:
-thread 2
-object 1
-
-links:
-
-thread 0 -- object 0
-thread 1 -- object 0
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/dme-mult.amf 2010-03-25 17:52:38 UTC (rev 25)
@@ -43,6 +43,6 @@
}
}
-initial-config {
+initialconfig {
( forward 0 SND )
}
Deleted: trunk/examples/dme-mult.topo
===================================================================
--- trunk/examples/dme-mult.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/dme-mult.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,12 +0,0 @@
-model: dme-mult.amf
-
-counts:
-forward 2
-critical 2
-
-links:
-
-critical0 -> forward0
-forward0 -> critical1
-critical1 -> forward1
-forward1 -> critical0
Modified: trunk/examples/dme.amf
===================================================================
--- trunk/examples/dme.amf 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/dme.amf 2010-03-25 17:52:38 UTC (rev 25)
@@ -33,6 +33,6 @@
}
}
-initial-config {
+initialconfig {
( node 0 SND )
}
Deleted: trunk/examples/dme.topo
===================================================================
--- trunk/examples/dme.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/dme.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,9 +0,0 @@
-model: dme.amf
-
-counts:
-node 2
-
-links:
-
-node0 -> node1
-node1 -> node0
Modified: trunk/examples/dpp.amf
===================================================================
--- trunk/examples/dpp.amf 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/dpp.amf 2010-03-25 17:52:38 UTC (rev 25)
@@ -63,5 +63,5 @@
}
}
-initial-config {
+initialconfig {
}
Deleted: trunk/examples/dpp.topo
===================================================================
--- trunk/examples/dpp.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/dpp.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,21 +0,0 @@
-#
-# dpp.topo
-#
-# describes the initial system instance
-# for dining philosophers protocol
-#
-
-# corresponding automata file
-model: dpp.amf
-
-# simple process counts
-counts:
-
-diner 2
-
-# explicit links between processes
-links:
-
-# simple ring
-diner 0 -> diner 1
-diner 1 -> diner 0
Deleted: trunk/examples/lr-dpp-11.topo
===================================================================
--- trunk/examples/lr-dpp-11.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/lr-dpp-11.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,32 +0,0 @@
-#
-# 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 1
-right-diner 1
-
-# 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 0 -> left-diner 0
-left-diner 0 -> right-diner 0
Deleted: trunk/examples/lr-dpp-22.topo
===================================================================
--- trunk/examples/lr-dpp-22.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/lr-dpp-22.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,35 +0,0 @@
-#
-# 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
Deleted: trunk/examples/lr-dpp-33.topo
===================================================================
--- trunk/examples/lr-dpp-33.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/lr-dpp-33.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,38 +0,0 @@
-#
-# 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 3
-right-diner 3
-
-# 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 2 -> left-diner 0
-
-left-diner 0 -> right-diner 0
-right-diner 0 -> left-diner 1
-
-left-diner 1 -> right-diner 1
-right-diner 1 -> left-diner 2
-
-left-diner 2 -> right-diner 2
Deleted: trunk/examples/lr-dpp-66.topo
===================================================================
--- trunk/examples/lr-dpp-66.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/lr-dpp-66.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,46 +0,0 @@
-#
-# 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 6
-right-diner 6
-
-# 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
-left-diner 0 -> right-diner 0
-right-diner 0 -> left-diner 1
-
-left-diner 1 -> right-diner 1
-right-diner 1 -> left-diner 2
-
-left-diner 2 -> right-diner 2
-right-diner 2 -> left-diner 3
-
-left-diner 3 -> right-diner 3
-right-diner 3 -> left-diner 4
-
-left-diner 4 -> right-diner 4
-right-diner 4 -> left-diner 5
-
-left-diner 5 -> right-diner 5
-right-diner 5 -> left-diner 0
Deleted: trunk/examples/lr-dpp-88.topo
===================================================================
--- trunk/examples/lr-dpp-88.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/lr-dpp-88.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,51 +0,0 @@
-#
-# 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 8
-right-diner 8
-
-# 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 7 -> left-diner 0
-
-left-diner 0 -> right-diner 0
-right-diner 0 -> left-diner 1
-
-left-diner 1 -> right-diner 1
-right-diner 1 -> left-diner 2
-
-left-diner 2 -> right-diner 2
-right-diner 2 -> left-diner 3
-
-left-diner 3 -> right-diner 3
-right-diner 3 -> left-diner 4
-
-left-diner 4 -> right-diner 4
-right-diner 4 -> left-diner 5
-
-left-diner 5 -> right-diner 5
-right-diner 5 -> left-diner 6
-
-left-diner 6 -> right-diner 6
-right-diner 6 -> left-diner 7
Modified: trunk/examples/lr-dpp.amf
===================================================================
--- trunk/examples/lr-dpp.amf 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/lr-dpp.amf 2010-03-25 17:52:38 UTC (rev 25)
@@ -125,5 +125,5 @@
# all right processes start in the first listed
# right process state
# (init in the automaton RIGHT-START)
-initial-config {
+initialconfig {
}
Deleted: trunk/examples/lr-dpp.topo
===================================================================
--- trunk/examples/lr-dpp.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/lr-dpp.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1 +0,0 @@
-link lr-dpp-22.topo
\ No newline at end of file
Deleted: trunk/examples/milners.topo
===================================================================
--- trunk/examples/milners.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/milners.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,10 +0,0 @@
-model: milners.amf
-
-counts:
-scheduler 2
-
-links:
-
-scheduler0 -> scheduler1
-scheduler1 -> scheduler0
-
Modified: trunk/examples/producer-consumer.amf
===================================================================
--- trunk/examples/producer-consumer.amf 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/producer-consumer.amf 2010-03-25 17:52:38 UTC (rev 25)
@@ -57,5 +57,5 @@
}
}
-initial-config {
+initialconfig {
}
Deleted: trunk/examples/producer-consumer.topo
===================================================================
--- trunk/examples/producer-consumer.topo 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/examples/producer-consumer.topo 2010-03-25 17:52:38 UTC (rev 25)
@@ -1,15 +0,0 @@
-model: producer-consumer.amf
-
-counts:
-
-producer 2
-consumer 2
-buffer 1
-
-links:
-
-producer 0 -- buffer 0
-producer 1 -- buffer 0
-
-consumer 0 -- buffer 0
-consumer 1 -- buffer 0
Modified: trunk/parser.scm
===================================================================
--- trunk/parser.scm 2010-03-25 16:20:53 UTC (rev 24)
+++ trunk/parser.scm 2010-03-25 17:52:38 UTC (rev 25)
@@ -90,7 +90,7 @@
(name-end ( number ) number-name-end)
(name-end ( identifier) variable-name-end)
- (initial-config ( "initial-config" "{" (arbno "(" start-spec ")" ) "}" ) the-initial-config)
+ (initial-config ( "initialconfig" "{" (arbno "(" start-spec ")" ) "}" ) the-initial-config)
(start-spec (identifier number identifier) a-start-spec)
))
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-03-25 16:20:59
|
Revision: 24
http://golok.svn.sourceforge.net/golok/?rev=24&view=rev
Author: sralmai
Date: 2010-03-25 16:20:53 +0000 (Thu, 25 Mar 2010)
Log Message:
-----------
[RELEASE PACKAGING]: version 1.2 candidate
Modified Paths:
--------------
trunk/README
trunk/golok.scm
Modified: trunk/README
===================================================================
--- trunk/README 2010-03-25 15:06:29 UTC (rev 23)
+++ trunk/README 2010-03-25 16:20:53 UTC (rev 24)
@@ -1,13 +1,37 @@
README
------
-README this file
-examples/ various example inputs to the program
+Golok is an automated tool for discovering the cut-off
+system instance size of parameterized systems.
-To run the examples, execute
+FILES
+-----
- ./golok <example file>
+README this file
+examples/ various example inputs to the program
+bin/ contains golok binary
+lib/ support files
+
+AUTHOR
+------
+David Samuelson
+sr...@ia...
+
+Please include "[Golok]" in the subject line.
+
+INSTALL
+-------
+Unpack golok-vx.x.tar.bz2.
+
+The binary was built on a Fedora 10 (Cambridge) x86 machine.
+It *should* work on most modern x86 GNU/Linux distributions.
+
+To run an example and output the simulating subset of the
+system instance, execute
+
+ ./golok --sys <example file>
+
You probably want to use GraphViz (http://www.graphviz.org)
to convert the .dot output files to images. Then you can
run a command like
@@ -17,37 +41,35 @@
to see the simulating subgraph of the solution as an svg
graphic.
-AUTHOR
-------
-David Samuelson
-sr...@ia...
+Execute
-INSTALL
--------
-Unpack golok-vx.x.tgz.
+ ./golok --help
-compile the tool using the mzscheme compiler
-(included in PLT Scheme)
+to see all command line options, and see the documentation
+at http://www.cs.iastate.edu/~slede/golok/ for more
+detailed usage of the tool.
-mzc --exe golok golok.scm
+NEWS
+---------
+v1.2
+----
+ * input format modified
-For example, to supress output of 1e models and dump
-program output into the directory "output", use
+ * many new command line options
-./golok -- --no-1e -o output <amf file>
+ * internals cleaned
-ChangeLog
+ * default behavior changed
+
---------
-v0.1.3.0
+v1.1.2
------
- * first published on sourceforge
+ * moved to sourceforge
* complete rewrite of low-level logic
- * versioning bump
-
---------
-v1.2.0
+v1.1.1
------
* added support for multiple parameterized processes
@@ -99,4 +121,5 @@
----
None known.
-Please contact the author with a description of the problem if you discover a bug.
+Please file a bug report at http://sourceforge.net/projects/golok/support if
+you discover a problem.
Modified: trunk/golok.scm
===================================================================
--- trunk/golok.scm 2010-03-25 15:06:29 UTC (rev 23)
+++ trunk/golok.scm 2010-03-25 16:20:53 UTC (rev 24)
@@ -8,7 +8,7 @@
(require scheme/cmdline)
;; version header -- should be in form vx.y.z(-tag)
- (define version "v0.1.4.0")
+ (define version "v1.2.0")
; parsed values of command line arguments
; currently size 11
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-03-25 15:06:38
|
Revision: 23
http://golok.svn.sourceforge.net/golok/?rev=23&view=rev
Author: sralmai
Date: 2010-03-25 15:06:29 +0000 (Thu, 25 Mar 2010)
Log Message:
-----------
[CLEANUP]: removed debugging line from dme-mult
Modified Paths:
--------------
trunk/examples/dme-mult.amf
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-03-25 15:03:43 UTC (rev 22)
+++ trunk/examples/dme-mult.amf 2010-03-25 15:06:29 UTC (rev 23)
@@ -37,7 +37,6 @@
}
msgs {
- ( critical, token2, peer)
( critical, token2, lpeer)
( critical, in, self)
( forward, token, lpeer)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-03-25 15:03:54
|
Revision: 22
http://golok.svn.sourceforge.net/golok/?rev=22&view=rev
Author: sralmai
Date: 2010-03-25 15:03:43 +0000 (Thu, 25 Mar 2010)
Log Message:
-----------
[PARSER CHANGE]: Depreciated "->" for describing links, now "--" is used for referencing "lpeer" "rpeer" and "peer" directional links. (dme-mult works again...)
Modified Paths:
--------------
trunk/examples/dme-mult.amf
trunk/examples/dme.amf
trunk/examples/dpp.amf
trunk/examples/lr-dpp.amf
trunk/examples/milners.amf
trunk/parser.scm
trunk/run-all.sh
trunk/search.scm
trunk/topo-datatypes.scm
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/examples/dme-mult.amf 2010-03-25 15:03:43 UTC (rev 22)
@@ -5,39 +5,39 @@
# "normal" nodes and pass nodes (as in "Automating Cut-off..")
#
#
-process forward {
-IDLE: [ Idle, token] -> [ Idle, token2]
-SND: [Start, epsilon] -> [Idle, token2]
-}
-
process critical {
ENTER: [ Idle, token2 ] -> [ Cs , in ]
LEAVE: [ Cs , in ] -> [ Idle , token ]
}
-# insert two new elements (a pass and a node) into the ring
+process forward {
+IDLE: [ Idle, token ] -> [ Idle, token2 ]
+SND: [ Start, epsilon ] -> [ Idle, token2 ]
+}
topology {
connectivity {
- critical 0 -> forward 0
- forward 0 -> critical 0
+ critical 0 -- forward 0
+ forward 0 -- critical 0
}
+ # insert two new elements (a forward and a critical) into the ring
additionrule plain-add {
create: critical x
create: forward y
- require: forward a -> critical 0
+ require: forward a -- critical 0
- remove: var a -> critical 0
+ remove: var a -- critical 0
- add: var a -> var x
- add: var x -> var y
- add: var y -> critical 0
+ add: var a -- var x
+ add: var x -- var y
+ add: var y -- critical 0
}
msgs {
+ ( critical, token2, peer)
( critical, token2, lpeer)
( critical, in, self)
( forward, token, lpeer)
Modified: trunk/examples/dme.amf
===================================================================
--- trunk/examples/dme.amf 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/examples/dme.amf 2010-03-25 15:03:43 UTC (rev 22)
@@ -1,5 +1,5 @@
#
-# gen-DME.amf
+# dme.amf
#
#
process node {
@@ -15,15 +15,15 @@
topology {
connectivity {
- node 0 -> node 0
+ node 0 -- node 0
}
additionrule plain-add {
- require: node y -> node 0
+ require: node y -- node 0
create: node x
- remove: var y -> node 0
- add: var y -> var x
- add: var x -> node 0
+ remove: var y -- node 0
+ add: var y -- var x
+ add: var x -- node 0
}
msgs {
Modified: trunk/examples/dpp.amf
===================================================================
--- trunk/examples/dpp.amf 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/examples/dpp.amf 2010-03-25 15:03:43 UTC (rev 22)
@@ -25,15 +25,15 @@
topology {
connectivity {
- diner 0 -> diner 0
+ diner 0 -- diner 0
}
additionrule add-one {
create: diner x
- require: diner y -> diner 0
- remove: var y -> diner 0
- add: var y -> var x
- add: var x -> diner 0
+ require: diner y -- diner 0
+ remove: var y -- diner 0
+ add: var y -- var x
+ add: var x -- diner 0
}
msgs {
Modified: trunk/examples/lr-dpp.amf
===================================================================
--- trunk/examples/lr-dpp.amf 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/examples/lr-dpp.amf 2010-03-25 15:03:43 UTC (rev 22)
@@ -52,19 +52,19 @@
topology {
connectivity {
- left-diner 0 -> right-diner 0
- right-diner 0 -> left-diner 0
+ left-diner 0 -- right-diner 0
+ right-diner 0 -- left-diner 0
}
# add another left and right diner into the ring
additionrule add-two {
create: left-diner x
create: right-diner y
- require: right-diner z -> left-diner 0
- remove: var z -> left-diner 0
- add: var z -> var x
- add: var x -> var y
- add: var y -> left-diner 0
+ require: right-diner z -- left-diner 0
+ remove: var z -- left-diner 0
+ add: var z -- var x
+ add: var x -- var y
+ add: var y -- left-diner 0
}
# the general format is:
Modified: trunk/examples/milners.amf
===================================================================
--- trunk/examples/milners.amf 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/examples/milners.amf 2010-03-25 15:03:43 UTC (rev 22)
@@ -25,16 +25,16 @@
topology {
connectivity {
- scheduler 0 -> scheduler 1
- scheduler 1 -> scheduler 0
+ scheduler 0 -- scheduler 1
+ scheduler 1 -- scheduler 0
}
additionrule plain-add {
- require: scheduler y -> scheduler 0
+ require: scheduler y -- scheduler 0
create: scheduler x
- remove: var y -> scheduler 0
- add: var y -> var x
- add: var x -> scheduler 0
+ remove: var y -- scheduler 0
+ add: var y -- var x
+ add: var x -- scheduler 0
}
msgs {
Modified: trunk/parser.scm
===================================================================
--- trunk/parser.scm 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/parser.scm 2010-03-25 15:03:43 UTC (rev 22)
@@ -193,8 +193,9 @@
(define-datatype
p_transition
p_transition?
- (a-p_transition (msg symbol?)
+ (a-p_transition
(process-type symbol?)
+ (msg symbol?)
(from-what-link-type symbol?)))
(define-datatype
Modified: trunk/run-all.sh
===================================================================
--- trunk/run-all.sh 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/run-all.sh 2010-03-25 15:03:43 UTC (rev 22)
@@ -2,7 +2,7 @@
# this *should* be something nice to ensure stuff works
-TESTS="dme SpinLock SpinLock-mult dpp lr-dpp"
+TESTS="dme dme-mult SpinLock SpinLock-mult dpp lr-dpp"
make clean
make
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/search.scm 2010-03-25 15:03:43 UTC (rev 22)
@@ -337,7 +337,7 @@
(let ([fr (hash-map fringe (lambda (x y) x))])
(cond
; if fringe empty, return fail
- ((= 0 (length fr)) (begin (display-ln "AM I ever here?\n")#f))
+ ((= 0 (length fr)) #f)
; return fringe
((= 0 depth) fringe) ;(begin (display-ln "The state space is " (hash-count state-space)"\n")fringe))
Modified: trunk/topo-datatypes.scm
===================================================================
--- trunk/topo-datatypes.scm 2010-03-24 15:42:06 UTC (rev 21)
+++ trunk/topo-datatypes.scm 2010-03-25 15:03:43 UTC (rev 22)
@@ -168,6 +168,12 @@
(env x)))))
; return a topo-vector for model-builder
+;
+; output is a vector of size # processes in topology
+;
+; each entry is a list of duples
+; (msg index-of-process-this-message-can-be-sent-to)
+;
(define topology-instantiate
(lambda (topo prot-msgs)
(let* ([ot (make-offset-table (topology-counts topo))]
@@ -179,7 +185,7 @@
(vector-ref model x)
prot-msgs vect (ot_ri2pt x ot)))
(build-list size values))])
- vect)))
+ vect)))
(define make-msg-list!
(lambda (x type-list prot-msgs vect pt)
@@ -224,8 +230,11 @@
(cons-to-vec vect r2 (list 'child p1 r1))))
((eqv? lt '--) (begin
(cons-to-vec vect r1 (list 'peer p2 r2))
- (cons-to-vec vect r2 (list 'peer p1 r1))))
+ (cons-to-vec vect r2 (list 'peer p1 r1)))
+ (cons-to-vec vect r1 (list 'lpeer p2 r2))
+ (cons-to-vec vect r2 (list 'rpeer p1 r1)))
((eqv? lt '->) (begin
+ (display-ln "WARNING: '->' is depreciated! Use '--' instead")
(cons-to-vec vect r1 (list 'lpeer p2 r2))
(cons-to-vec vect r2 (list 'rpeer p1 r1))))
(#t (raise-user-error (string-append "Parse error: "
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-03-24 15:42:14
|
Revision: 21
http://golok.svn.sourceforge.net/golok/?rev=21&view=rev
Author: sralmai
Date: 2010-03-24 15:42:06 +0000 (Wed, 24 Mar 2010)
Log Message:
-----------
[PARSER CHANGE][BROKEN COMMIT]: modified parser to follow the tool paper "topology" section. dme-mult does NOT work (but the part that is most likely the problem will be revamped in the next commit)
Modified Paths:
--------------
trunk/examples/SpinLock-mult.amf
trunk/examples/SpinLock.amf
trunk/examples/dme-mult.amf
trunk/examples/dme.amf
trunk/examples/dpp.amf
trunk/examples/lr-dpp.amf
trunk/examples/milners.amf
trunk/examples/producer-consumer.amf
trunk/find-k.scm
trunk/parser.scm
trunk/run-all.sh
Modified: trunk/examples/SpinLock-mult.amf
===================================================================
--- trunk/examples/SpinLock-mult.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/SpinLock-mult.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -1,11 +1,8 @@
#
-# SpinLock.amf
+# SpinLock-mult.amf
#
-# automata file for Spin Lock
+# automata file for Spin Lock with multiple locks
#
-# David Samuelson
-# August 4, 2009
-#
process thread {
START: [initial, epsilon ] -> [ Start, begin ]
@@ -23,32 +20,40 @@
}
-addition-rule add-thread {
- create: thread x
- foreach object y
- {
- add: var x -- var y
+
+topology {
+ connectivity {
+ thread 0 -- object 0
+ thread 0 -- object 1
+ thread 1 -- object 0
+ thread 1 -- object 1
}
-}
-addition-rule add-object {
- create: object x
- foreach thread y {
- add: var x -- var y
+ additionrule add-thread {
+ create: thread x
+ foreach object y
+ {
+ add: var x -- var y
+ }
}
-}
+
+ additionrule add-object {
+ create: object x
+ foreach thread y {
+ add: var x -- var y
+ }
+ }
-topology {
- (object, req, peer)
- (object, rel, peer)
- (thread, in, self)
- (thread, ack, peer)
- (thread, nack, peer)
- (thread, begin, peer)
- (thread, begin, self)
+ msgs {
+ (object, req, peer)
+ (object, rel, peer)
+ (thread, in, self)
+ (thread, ack, peer)
+ (thread, nack, peer)
+ (thread, begin, peer)
+ (thread, begin, self)
+ }
}
initial-config {
}
-
-kernel = SpinLock-mult.topo
Modified: trunk/examples/SpinLock.amf
===================================================================
--- trunk/examples/SpinLock.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/SpinLock.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -20,25 +20,30 @@
}
+topology {
+ connectivity {
+ thread 0 -- object 0
+ thread 1 -- object 0
+ }
-addition-rule add-thread {
- create: thread x
- foreach object y
- {
- add: var x -- var y
+ additionrule add-thread {
+ create: thread x
+ foreach object y
+ {
+ add: var x -- var y
+ }
}
+
+ msgs {
+ (object, req, peer)
+ (object, rel, peer)
+ (thread, in, self)
+ (thread, ack, peer)
+ (thread, nack, peer)
+ (thread, begin, peer)
+ (thread, begin, self)
+ }
}
-topology {
- (object, req, peer)
- (object, rel, peer)
- (thread, in, self)
- (thread, ack, peer)
- (thread, nack, peer)
- (thread, begin, peer)
- (thread, begin, self)
-}
initial-config {
}
-
-kernel = SpinLock.topo
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/dme-mult.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -1,5 +1,5 @@
#
-# dme-multi.amf
+# dme-mult.amf
#
# implementation of distributed mutual exclusion with
# "normal" nodes and pass nodes (as in "Automating Cut-off..")
@@ -17,27 +17,33 @@
}
# insert two new elements (a pass and a node) into the ring
-addition-rule plain-add {
- require: forward a -> critical 0
- create: critical x
- create: forward y
+topology {
+ connectivity {
+ critical 0 -> forward 0
+ forward 0 -> critical 0
+ }
+
+ additionrule plain-add {
+ create: critical x
+ create: forward y
+
+ require: forward a -> critical 0
- remove: var a -> critical 0
-
- add: var a -> var x
- add: var x -> var y
- add: var y -> critical 0
+ remove: var a -> critical 0
+
+ add: var a -> var x
+ add: var x -> var y
+ add: var y -> critical 0
+ }
+
+ msgs {
+ ( critical, token2, lpeer)
+ ( critical, in, self)
+ ( forward, token, lpeer)
+ }
}
-topology {
- ( critical, token2, lpeer)
- ( critical, in, self)
- ( forward, token, lpeer)
-}
-
initial-config {
( forward 0 SND )
}
-
-kernel = dme-mult.topo
Modified: trunk/examples/dme.amf
===================================================================
--- trunk/examples/dme.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/dme.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -11,22 +11,28 @@
}
-addition-rule plain-add {
- require: node y -> node 0
- create: node x
- remove: var y -> node 0
- add: var y -> var x
- add: var x -> node 0
-}
topology {
- ( node, token, lpeer)
- ( node, in, self)
- ( node, choose, self)
+
+ connectivity {
+ node 0 -> node 0
+ }
+
+ additionrule plain-add {
+ require: node y -> node 0
+ create: node x
+ remove: var y -> node 0
+ add: var y -> var x
+ add: var x -> node 0
+ }
+
+ msgs {
+ ( node, token, lpeer)
+ ( node, in, self)
+ ( node, choose, self)
+ }
}
initial-config {
( node 0 SND )
}
-
-kernel = dme.topo
Modified: trunk/examples/dpp.amf
===================================================================
--- trunk/examples/dpp.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/dpp.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -3,8 +3,6 @@
#
# behavioral automata for dining philosophers protocol
#
-# (for golok v1.2.0)
-#
process diner {
BEGIN: [init, epsilon ] -> [ not-eating, begin ]
@@ -24,41 +22,46 @@
EAT_DONE: [eat, rel_forks] -> [not-eating, begin]
}
-addition-rule add-one {
- create: diner x
- require: diner y -> diner 0
- remove: var y -> diner 0
- add: var y -> var x
- add: var x -> diner 0
-}
topology {
-# (begin, i, i)
-(diner, begin, self)
-
-# (ask_left, i, i - 1)
-(diner, ask_left, rpeer)
-
-# (left_taken, i , i + 1)
-(diner, left_taken, lpeer)
-
-# (left_free, i, i + 1)
-(diner, left_free, lpeer)
-
-# (ask_right, i, i + 1)
-(diner, ask_right, lpeer)
-
-# (right_taken, i , i -1 )
-(diner, right_taken, rpeer)
-
-# (right_free, i, i -1)
-(diner, right_free, rpeer)
-
-# (rel_forks, i, i)
-(diner, rel_forks, self)
+ connectivity {
+ diner 0 -> diner 0
+ }
+
+ additionrule add-one {
+ create: diner x
+ require: diner y -> diner 0
+ remove: var y -> diner 0
+ add: var y -> var x
+ add: var x -> diner 0
+ }
+
+ msgs {
+ # (begin, i, i)
+ (diner, begin, self)
+
+ # (ask_left, i, i - 1)
+ (diner, ask_left, rpeer)
+
+ # (left_taken, i , i + 1)
+ (diner, left_taken, lpeer)
+
+ # (left_free, i, i + 1)
+ (diner, left_free, lpeer)
+
+ # (ask_right, i, i + 1)
+ (diner, ask_right, lpeer)
+
+ # (right_taken, i , i -1 )
+ (diner, right_taken, rpeer)
+
+ # (right_free, i, i -1)
+ (diner, right_free, rpeer)
+
+ # (rel_forks, i, i)
+ (diner, rel_forks, self)
+ }
}
initial-config {
}
-
-kernel = dpp.topo
Modified: trunk/examples/lr-dpp.amf
===================================================================
--- trunk/examples/lr-dpp.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/lr-dpp.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -49,61 +49,69 @@
EAT-DONE2: [eat, rel-forks2] -> [not-eating, begin2]
}
-# add another left and right diner into the ring
-addition-rule add-two {
- create: left-diner x
- create: right-diner y
- require: right-diner z -> left-diner 0
- remove: var z -> left-diner 0
- add: var z -> var x
- add: var x -> var y
- add: var y -> left-diner 0
-}
topology {
-# the general format is:
-#
-# ( process-type, message, link-position )
-#
-
-# (ask-left, i_diner, i-1_diner)
-#
-# this first rule means
-# a left-diner process can receive an
-# ask-left message from is right peer
-#
-# (see lr-dpp.topo for the meaning of
-# right peer)
- (left-diner, ask-left, rpeer)
- (right-diner, ask-left2, rpeer)
-
-# (left-taken, i_diner, i+1_diner)
- (left-diner, left-taken, lpeer)
- (right-diner, left-taken2, lpeer)
-
-# (left-free, i_diner, i+1_diner)
- (left-diner, left-free, lpeer)
- (right-diner, left-free2, lpeer)
-
-# (ask-right, i_diner, i+1_diner)
- (left-diner, ask-right, lpeer)
- (right-diner, ask-right2, lpeer)
-
-# (right-taken, i_diner, i-1_diner)
- (left-diner, right-taken, rpeer)
- (right-diner, right-taken2, rpeer)
-
-# (right-free, i_diner, i-1_diner)
- (left-diner, right-free, rpeer)
- (right-diner, right-free2, rpeer)
-
-# (rel-forks, i_diner, i_diner)
- (left-diner, rel-forks, self)
- (right-diner, rel-forks2, self)
-
-# (self start messages)
- (left-diner, begin, self)
- (right-diner, begin2, self)
+ connectivity {
+ left-diner 0 -> right-diner 0
+ right-diner 0 -> left-diner 0
+ }
+
+ # add another left and right diner into the ring
+ additionrule add-two {
+ create: left-diner x
+ create: right-diner y
+ require: right-diner z -> left-diner 0
+ remove: var z -> left-diner 0
+ add: var z -> var x
+ add: var x -> var y
+ add: var y -> left-diner 0
+ }
+
+ # the general format is:
+ #
+ # ( process-type, message, link-position )
+ #
+
+ # (ask-left, i_diner, i-1_diner)
+ #
+ # this first rule means
+ # a left-diner process can receive an
+ # ask-left message from is right peer
+ #
+ # (see lr-dpp.topo for the meaning of
+ # right peer)
+ msgs {
+ (left-diner, ask-left, rpeer)
+ (right-diner, ask-left2, rpeer)
+
+ # (left-taken, i_diner, i+1_diner)
+ (left-diner, left-taken, lpeer)
+ (right-diner, left-taken2, lpeer)
+
+ # (left-free, i_diner, i+1_diner)
+ (left-diner, left-free, lpeer)
+ (right-diner, left-free2, lpeer)
+
+ # (ask-right, i_diner, i+1_diner)
+ (left-diner, ask-right, lpeer)
+ (right-diner, ask-right2, lpeer)
+
+ # (right-taken, i_diner, i-1_diner)
+ (left-diner, right-taken, rpeer)
+ (right-diner, right-taken2, rpeer)
+
+ # (right-free, i_diner, i-1_diner)
+ (left-diner, right-free, rpeer)
+ (right-diner, right-free2, rpeer)
+
+ # (rel-forks, i_diner, i_diner)
+ (left-diner, rel-forks, self)
+ (right-diner, rel-forks2, self)
+
+ # (self start messages)
+ (left-diner, begin, self)
+ (right-diner, begin2, self)
+ }
}
# no special configuration
@@ -119,5 +127,3 @@
# (init in the automaton RIGHT-START)
initial-config {
}
-
-kernel = lr-dpp.topo
Modified: trunk/examples/milners.amf
===================================================================
--- trunk/examples/milners.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/milners.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -22,23 +22,28 @@
}
-addition-rule plain-add {
- require: scheduler y -> scheduler 0
- create: scheduler x
- remove: var y -> scheduler 0
- add: var y -> var x
- add: var x -> scheduler 0
-}
topology {
- (scheduler,token,lpeer)
- (scheduler,compute,self)
- (scheduler,send-token,self)
+ connectivity {
+ scheduler 0 -> scheduler 1
+ scheduler 1 -> scheduler 0
+ }
+
+ additionrule plain-add {
+ require: scheduler y -> scheduler 0
+ create: scheduler x
+ remove: var y -> scheduler 0
+ add: var y -> var x
+ add: var x -> scheduler 0
+ }
+
+ msgs {
+ (scheduler,token,lpeer)
+ (scheduler,compute,self)
+ (scheduler,send-token,self)
+ }
}
-initial-config{
+initialconfig{
( scheduler 0 INIT )
}
-
-kernel = milners.topo
-
Modified: trunk/examples/producer-consumer.amf
===================================================================
--- trunk/examples/producer-consumer.amf 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/examples/producer-consumer.amf 2010-03-24 15:42:06 UTC (rev 21)
@@ -1,16 +1,16 @@
process producer {
-init: [Init, epsilon] -> [Produced, item]
-produced: [Produced, item] -> [AddBuffer, putprod]
-addbuffernak: [AddBuffer, bufferNAKprod] -> [AddBuffer, putprod]
-addbufferok: [AddBuffer, bufferOKprod] -> [Produced, item]
+ init: [Init, epsilon] -> [Produced, item]
+ produced: [Produced, item] -> [AddBuffer, putprod]
+ addbuffernak: [AddBuffer, bufferNAKprod] -> [AddBuffer, putprod]
+ addbufferok: [AddBuffer, bufferOKprod] -> [Produced, item]
}
process consumer {
-init2: [Init2, epsilon] -> [GetBuffer, getcons]
-getnak2: [GetBuffer, bufferNAKcons] -> [GetBuffer, getcons]
-getok2: [GetBuffer, bufferOKcons] -> [HasConsumed, in]
-inleave: [HasConsumed, in] -> [GetBuffer, getcons]
+ init2: [Init2, epsilon] -> [GetBuffer, getcons]
+ getnak2: [GetBuffer, bufferNAKcons] -> [GetBuffer, getcons]
+ getok2: [GetBuffer, bufferOKcons] -> [HasConsumed, in]
+ inleave: [HasConsumed, in] -> [GetBuffer, getcons]
}
process buffer {
@@ -24,29 +24,38 @@
}
-addition-rule add-producer {
- create: producer x
- add: var x -- buffer 0
-}
-#addition-rule add-consumer {
-# create: consumer x
-# add: var x -- buffer 0
-#}
-
topology {
- (producer, item, self)
- (consumer, in, self)
- (producer, bufferOKprod, peer)
- (producer, bufferNAKprod, peer)
- (consumer, bufferOKcons, peer)
- (consumer, bufferNAKcons, peer)
- (buffer, putprod, peer)
- (buffer, getcons, peer)
+ connectivity {
+ producer 0 -- buffer 0
+ producer 1 -- buffer 0
+ consumer 0 -- buffer 0
+ consumer 1 -- buffer 0
+ }
+
+ additionrule add-producer {
+ create: producer x
+ add: var x -- buffer 0
+ }
+
+ additionrule add-consumer {
+ create: consumer x
+ add: var x -- buffer 0
+ }
+
+ msgs {
+ (producer, item, self)
+ (consumer, in, self)
+ (producer, bufferOKprod, peer)
+ (producer, bufferNAKprod, peer)
+ (consumer, bufferOKcons, peer)
+ (consumer, bufferNAKcons, peer)
+
+ (buffer, putprod, peer)
+ (buffer, getcons, peer)
+ }
}
initial-config {
}
-
-kernel = producer-consumer.topo
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/find-k.scm 2010-03-24 15:42:06 UTC (rev 21)
@@ -139,7 +139,7 @@
(set! start-time (current-seconds))
; k is current system instance
- (set! k (file->topology (string-append amf-directory (protocol-kernel prot))))))))
+ (set! k (protocol-kernel prot))))))
(define parse-filename
(lambda (fn)
Modified: trunk/parser.scm
===================================================================
--- trunk/parser.scm 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/parser.scm 2010-03-24 15:42:06 UTC (rev 21)
@@ -61,15 +61,17 @@
'((whitespace (whitespace) skip)
(comment ("#" (arbno (not #\newline))) skip)
(identifier (letter (arbno (or letter digit "." "_" "/" "-" "?"))) symbol)
- ; (link ("-" (or "-" "E" ">")) symbol)
(number ((or digit "-") (arbno digit)) number)))
(define the-grammar
- '((p_protocol ((arbno "process" p_process) (arbno "addition-rule" addition-rule) p_topology initial-config "kernel" "=" identifier) a-prot)
+ '((p_protocol ((arbno "process" p_process) p_topology initial-config) a-prot)
(p_process (identifier "{" (arbno automaton) "}") a-process)
(automaton (identifier ":" "[" identifier "," identifier "]" "->" "[" identifier "," identifier "]" ) simple-automaton)
+ ;; link is a single entry in the connectivity table
+ (p_link (identifier number link identifier number) a-link)
- (p_topology ( "topology " "{" (arbno p_transition) "}" ) a-p_topology)
+ (p_topology ( "topology " "{" "connectivity" "{" (arbno p_link) "}" (arbno "additionrule" addition-rule) "msgs" "{" (arbno p_transition) "}" "}" ) a-p_topology)
+
(p_transition ("(" identifier "," identifier "," identifier ")") a-p_transition)
(addition-rule (identifier "{" (arbno p_expr) "}") an-addition-rule)
@@ -100,13 +102,23 @@
(link_type link?)
(n2 name?)))
- (define-datatype
- link
- link?
- (peer-link)
- (directed-link)
- (pc-link))
+(define-datatype
+ link
+ link?
+ (peer-link)
+ (directed-link)
+ (pc-link))
+(define-datatype
+ p_link
+ p_link?
+ (a-link
+ (p1 symbol?)
+ (i1 number?)
+ (lt link?)
+ (p2 symbol?)
+ (i2 number?)))
+
(define-datatype
addition-rule
addition-rule?
@@ -158,10 +170,9 @@
p_protocol?
(a-prot
(proc-list (list-of p_process?))
- (add-rule-list (list-of addition-rule?))
(topo p_topology?)
- (init initial-config?)
- (kernel symbol?)))
+ (init initial-config?)))
+
(define-datatype
p_process
@@ -175,8 +186,10 @@
p_topology
p_topology?
(a-p_topology
+ (links (list-of p_link?))
+ (add-rules (list-of addition-rule?))
(trans (list-of p_transition?))))
-
+
(define-datatype
p_transition
p_transition?
@@ -258,29 +271,29 @@
;; read a protocol and return a protocol structure
;;
(define parseProtocol
- (lambda (prot)
+ (lambda (prot filename)
(cases p_protocol prot
- (a-prot (p_processes p_add-rules topo_r init kernel)
- (begin
+ (a-prot (p_processes topo_r init)
+ (cases p_topology topo_r
+ (a-p_topology (p_links p_add-rules p_transitions)
+ (begin
; first do some quick sanity checks
(if (zero? (length p_processes)) (raise-user-error 'PARSE "no processes defined!") (void))
(if (zero? (length p_add-rules)) (raise-user-error 'PARSE "no addition rules defined!") (void))
-
(let* ([procs (map p_proc2proc p_processes)]
[add-rules (map parse-rule p_add-rules)]
- [the-topo (parse-topo topo_r)]
+ [the-topo (parse-topo p_transitions)]
[names (map process-name procs)]
[auts (list-of-lists->list
(map process-auts procs))]
- [start (parse-init init auts)])
- (make-protocol names procs add-rules the-topo start (symbol->string kernel))))))))
+ [start (parse-init init auts)]
+ [kernel (create-kernel filename p_links)])
+ (make-protocol names procs add-rules the-topo start kernel)))))))))
;; topology object -> list of allowed transitions
(define parse-topo
- (lambda (t)
- (cases p_topology t
- (a-p_topology (tr)
- (map trans-unpacker tr)))))
+ (lambda (tr)
+ (map trans-unpacker tr)))
(define trans-unpacker
(lambda (x)
@@ -294,6 +307,11 @@
(the-initial-config (loss)
(map (lambda (x) (parse-start-spec x auts)) loss)))))
+ (define parse_link
+ (lambda (ln)
+ (cases p_link ln
+ (a-link (id1 num1 lt id2 num2) (list id1 num1 (unwrap-lt lt) id2 num2)))))
+
(define parse-start-spec
(lambda (spec auts)
(cases start-spec spec
@@ -309,7 +327,7 @@
(define parse-amf-file
(lambda (x)
- (parseProtocol (s&p_file x))))
+ (parseProtocol (s&p_file x) x)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -488,7 +506,6 @@
(number-name-end (z) (list id z))
(variable-name-end (z) (list id z)))))))
-
; count the number of possible bindings for this requirement
(define count-options
(lambda (x t_links)
@@ -529,3 +546,40 @@
(lambda (x)
(if (eq? sym x) (list proc_t index)
(env x)))))
+
+;;
+;; (string? (list-of link?)) -> topology?
+;;
+(define (create-kernel filename p_links)
+ (let* ([links (map parse_link p_links)]
+ [counts (count-links links)])
+ (make-topology filename counts links)))
+
+;;
+;; (list-of link?
+;;
+(define (count-links links)
+ (let ([db (make-hash)])
+ (begin
+ (count-links-rec links db)
+ (hash-map db (lambda (x y) (list x y))))))
+
+(define (count-links-rec links db)
+ (if (null? links) (void)
+ (let* ([ln (car links)]
+ [name1 (car ln)]
+ [sz1 (second ln)]
+ [name2 (fourth ln)]
+ [sz2 (fifth ln)])
+ (begin
+ (process-link-entry name1 sz1 db)
+ (process-link-entry name2 sz2 db)
+ (count-links-rec (cdr links) db)))))
+
+(define (process-link-entry name sz db)
+ (if (not (hash-has-key? db name))
+ (hash-set! db name (add1 sz))
+ (let ([prev-sz (hash-ref db name)])
+ ;; if already have a larger count, ignore
+ (if (> prev-sz sz) (void)
+ (hash-set! db name (add1 sz))))))
Modified: trunk/run-all.sh
===================================================================
--- trunk/run-all.sh 2010-03-23 15:20:01 UTC (rev 20)
+++ trunk/run-all.sh 2010-03-24 15:42:06 UTC (rev 21)
@@ -2,7 +2,7 @@
# this *should* be something nice to ensure stuff works
-TESTS="dme dme-mult SpinLock-mult dpp lr-dpp"
+TESTS="dme SpinLock SpinLock-mult dpp lr-dpp"
make clean
make
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-03-23 15:20:07
|
Revision: 20
http://golok.svn.sourceforge.net/golok/?rev=20&view=rev
Author: sralmai
Date: 2010-03-23 15:20:01 +0000 (Tue, 23 Mar 2010)
Log Message:
-----------
[MINOR TWEAKS]: output files are now overwritten, and the Makefile includes topo-dataypes.scm
Modified Paths:
--------------
trunk/Makefile
trunk/model-builder.scm
trunk/run-all.sh
trunk/topo-datatypes.scm
Modified: trunk/Makefile
===================================================================
--- trunk/Makefile 2010-03-14 02:54:53 UTC (rev 19)
+++ trunk/Makefile 2010-03-23 15:20:01 UTC (rev 20)
@@ -1,4 +1,4 @@
-golok: lookup-table.scm datatypes.scm model-builder.scm search.scm golok.scm find-k.scm parser.scm
+golok: lookup-table.scm datatypes.scm model-builder.scm search.scm golok.scm find-k.scm parser.scm topo-datatypes.scm
mzc --exe golok golok.scm
render:
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-03-14 02:54:53 UTC (rev 19)
+++ trunk/model-builder.scm 2010-03-23 15:20:01 UTC (rev 20)
@@ -428,8 +428,7 @@
[mdl (model-mdl md)]
[proc-mask-ids (map (lambda (x) (proc->proc-id x lookup-table)) process-mask)])
(begin
- (if (file-exists? filename) (raise-user-error "output file already exists:" filename) (void))
- (current-output-port (open-output-file filename))
+ (current-output-port (open-output-file filename #:exists 'replace))
(display-ln "/* model generated by model2dot */\n\ndigraph {\n\trankdir=LR\n\n")
(for-each (lambda (x) (entry2dot x (vector-ref mdl x) lookup-table proc-mask-ids sb?))
(build-list (vector-length mdl) values))
Modified: trunk/run-all.sh
===================================================================
--- trunk/run-all.sh 2010-03-14 02:54:53 UTC (rev 19)
+++ trunk/run-all.sh 2010-03-23 15:20:01 UTC (rev 20)
@@ -26,11 +26,10 @@
else
./golok -o output examples/$i.amf || fail
fi
- make clean
-##echo "Testing DFS"
- # ./golok -o output --dfs examples/$i.amf || fail
-# make clean
+#echo "Testing DFS"
+# ./golok -o output --dfs examples/$i.amf || fail
+# make clean
done
make clean
Modified: trunk/topo-datatypes.scm
===================================================================
--- trunk/topo-datatypes.scm 2010-03-14 02:54:53 UTC (rev 19)
+++ trunk/topo-datatypes.scm 2010-03-23 15:20:01 UTC (rev 20)
@@ -87,7 +87,8 @@
(display-ln (car x) " " (cadr x))) counts)
(display-ln "\nlinks:\n")
(for-each (lambda (x)
- (display-ln (car x) " " (cadr x) " " (caddr x) " " (fourth x) " " (fifth x))) links)))))))
+ (display-ln (car x) " " (cadr x) " " (caddr x) " " (fourth x) " " (fifth x))) links)))
+ 'replace))))
(define the-lexical-spec
'((whitespace (whitespace) skip)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ne...@us...> - 2010-03-14 02:55:00
|
Revision: 19
http://golok.svn.sourceforge.net/golok/?rev=19&view=rev
Author: nedgty
Date: 2010-03-14 02:54:53 +0000 (Sun, 14 Mar 2010)
Log Message:
-----------
[ADDED FEATURE] displaying the total number of explored states
Modified Paths:
--------------
trunk/examples/dme.amf
trunk/search.scm
Modified: trunk/examples/dme.amf
===================================================================
--- trunk/examples/dme.amf 2010-03-14 01:10:45 UTC (rev 18)
+++ trunk/examples/dme.amf 2010-03-14 02:54:53 UTC (rev 19)
@@ -29,4 +29,4 @@
( node 0 SND )
}
-kernel = dme-2.topo
+kernel = dme.topo
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-14 01:10:45 UTC (rev 18)
+++ trunk/search.scm 2010-03-14 02:54:53 UTC (rev 19)
@@ -73,6 +73,10 @@
;; hash-map of states already checked for simulation (keys: system-states, values: #t)
(define state-space #f)
+;; hash-map to save the number of explored states for the sake of writing the
+;; results in the paper
+(define states-explored 0)
+
;; filter for checking a state for simulation (this is a heuristic)
;; TODO: implement this (since we changed to state-based instead of
;; automaton-based representation, this is harder to do)
@@ -225,7 +229,8 @@
(values #t result)))
(result
(begin
- (display-ln "This is simulating done" (vector-length result) "\n")
+ ;(display-ln "This is simulating done" (vector-length result) "\n")
+ (display-ln "The number of explored states is " (hash-count states-explored) "\n")
(values #t (search->model result))))
; otherwise just return failure
(#t
@@ -270,6 +275,7 @@
(begin
; reset the global space
(set! state-space (make-hash))
+ (set! states-explored (make-hash))
(search-bfs-rec depth (make-hash) dump))))
(define search-bfs-rec
@@ -324,6 +330,8 @@
; expand once and return results
(get-fringe-rec state-space fringe 1))))
+; this is basically called once since the parameter of depth is "1"
+; and then the fringe is returned
(define get-fringe-rec
(lambda (state-space fringe depth)
(let ([fr (hash-map fringe (lambda (x y) x))])
@@ -332,7 +340,7 @@
((= 0 (length fr)) (begin (display-ln "AM I ever here?\n")#f))
; return fringe
- ((= 0 depth) (begin (display-ln "The state space is " (hash-count state-space)"\n")fringe))
+ ((= 0 depth) fringe) ;(begin (display-ln "The state space is " (hash-count state-space)"\n")fringe))
; otherwise expand next
(#t
@@ -352,7 +360,7 @@
; add all states to state-space
(map (lambda (x)
(hash-set! state-space x #t)) possible-starts)
- (display-ln "The count of state space is "(hash-count state-space) "\n")
+ ;(display-ln "The count of state space is "(hash-count state-space) "\n")
(get-fringe-rec state-space new-fr (sub1 depth)))))))))
;;;;;;;;;;;;;;;;; end search ;;;;;;;;;;;;;;;;;;
@@ -414,7 +422,9 @@
; otherwise, lets assume this state simulates
(let ([new-em (make-vector (vector-length eq-map))])
(begin
- (display-ln "The number of children to explore are" (length check-list) "\n")
+ ;(display-ln "Check list has " check-list "\n")
+ (map (lambda(x) (hash-set! states-explored x #f)) check-list)
+ ;(display-ln "The number of children to explore are" (length check-list) "\n")
; first make a copy of the equivalence map
(vector-copy! new-em 0 eq-map)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ne...@us...> - 2010-03-14 01:10:56
|
Revision: 18
http://golok.svn.sourceforge.net/golok/?rev=18&view=rev
Author: nedgty
Date: 2010-03-14 01:10:45 +0000 (Sun, 14 Mar 2010)
Log Message:
-----------
Added some debug messages that helps getting the number of explored states
Modified Paths:
--------------
trunk/examples/dme.amf
trunk/search.scm
Modified: trunk/examples/dme.amf
===================================================================
--- trunk/examples/dme.amf 2010-03-12 07:35:08 UTC (rev 17)
+++ trunk/examples/dme.amf 2010-03-14 01:10:45 UTC (rev 18)
@@ -29,4 +29,4 @@
( node 0 SND )
}
-kernel = dme.topo
+kernel = dme-2.topo
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-12 07:35:08 UTC (rev 17)
+++ trunk/search.scm 2010-03-14 01:10:45 UTC (rev 18)
@@ -225,7 +225,7 @@
(values #t result)))
(result
(begin
- (display-ln "We are going to search now")
+ (display-ln "This is simulating done" (vector-length result) "\n")
(values #t (search->model result))))
; otherwise just return failure
(#t
@@ -258,7 +258,7 @@
[possible-starts (filter start-state-filter new-states)])
(begin
(hash-set! store state #t)
- (if (null? possible-starts) #f
+ (if (null? possible-starts) (begin (display-ln "The hash has " (hash-count store) " state \n") #f)
(ormap (lambda (x) (search-dfs-rec x store)) possible-starts)))))))))))
@@ -329,10 +329,10 @@
(let ([fr (hash-map fringe (lambda (x y) x))])
(cond
; if fringe empty, return fail
- ((= 0 (length fr)) #f)
+ ((= 0 (length fr)) (begin (display-ln "AM I ever here?\n")#f))
; return fringe
- ((= 0 depth) fringe)
+ ((= 0 depth) (begin (display-ln "The state space is " (hash-count state-space)"\n")fringe))
; otherwise expand next
(#t
@@ -352,6 +352,7 @@
; add all states to state-space
(map (lambda (x)
(hash-set! state-space x #t)) possible-starts)
+ (display-ln "The count of state space is "(hash-count state-space) "\n")
(get-fringe-rec state-space new-fr (sub1 depth)))))))))
;;;;;;;;;;;;;;;;; end search ;;;;;;;;;;;;;;;;;;
@@ -413,6 +414,7 @@
; otherwise, lets assume this state simulates
(let ([new-em (make-vector (vector-length eq-map))])
(begin
+ (display-ln "The number of children to explore are" (length check-list) "\n")
; first make a copy of the equivalence map
(vector-copy! new-em 0 eq-map)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ne...@us...> - 2010-03-12 07:35:18
|
Revision: 17
http://golok.svn.sourceforge.net/golok/?rev=17&view=rev
Author: nedgty
Date: 2010-03-12 07:35:08 +0000 (Fri, 12 Mar 2010)
Log Message:
-----------
[BUG FIX] fixed the problem that was causing producer-consumer not to work
Modified Paths:
--------------
trunk/examples/producer-consumer.amf
trunk/examples/producer-consumer.topo
trunk/search.scm
Modified: trunk/examples/producer-consumer.amf
===================================================================
--- trunk/examples/producer-consumer.amf 2010-03-11 18:12:37 UTC (rev 16)
+++ trunk/examples/producer-consumer.amf 2010-03-12 07:35:08 UTC (rev 17)
@@ -2,34 +2,17 @@
init: [Init, epsilon] -> [Produced, item]
produced: [Produced, item] -> [AddBuffer, putprod]
-#recvnak: [WaitMutex, mutexNAKprod] -> [WaitMutex, setprod]
-#recvok: [WaitMutex, mutexOKprod] -> [AddBuffer, putprod]
addbuffernak: [AddBuffer, bufferNAKprod] -> [AddBuffer, putprod]
addbufferok: [AddBuffer, bufferOKprod] -> [Produced, item]
-#recvmutexok: [ClearMutex, mutexCLEARprod] -> [Produced, item]
}
process consumer {
init2: [Init2, epsilon] -> [GetBuffer, getcons]
-#recvnak2: [WaitMutex, mutexNAKcons] -> [WaitMutex, setcons]
-#recvok2: [WaitMutex, mutexOKcons] -> [GetBuffer, getcons]
getnak2: [GetBuffer, bufferNAKcons] -> [GetBuffer, getcons]
-getok2: [GetBuffer, bufferOKcons] -> [HasCosumed, in]
-in: [HasConsumed, in] -> [GetBuffer, getcons]
-#recvreplay: [ClearMutex, mutexCLEARcons] -> [GetBuffer, getcons]
+getok2: [GetBuffer, bufferOKcons] -> [HasConsumed, in]
+inleave: [HasConsumed, in] -> [GetBuffer, getcons]
}
-# process mutex {
-# setpassprod: [Clear, setprod] -> [Set, mutexOKprod]
-# setfailprod: [Set, setprod] -> [Set, mutexNAKprod]
-# clearprod: [Set, clearprod] -> [Clear, mutexCLEARprod]
-
-# setpasscons: [Clear, setcons] -> [Set, mutexOKcons]
-# setfailcons: [Set, setcons] -> [Set, mutexNAKcons]
-# clearcons: [Set, clearcons] -> [Clear, mutexCLEARcons]
-# }
-
-
process buffer {
putzeroprod: [Zero, putprod] -> [One, bufferOKprod]
@@ -43,37 +26,23 @@
addition-rule add-producer {
create: producer x
-# add: var x -- mutex 0
add: var x -- buffer 0
}
-addition-rule add-consumer {
- create: consumer x
-# add: var x -- mutex 0
- add: var x -- buffer 0
-}
+#addition-rule add-consumer {
+# create: consumer x
+# add: var x -- buffer 0
+#}
topology {
(producer, item, self)
(consumer, in, self)
(producer, bufferOKprod, peer)
(producer, bufferNAKprod, peer)
-# (producer, mutexOKprod, peer)
-# (producer, mutexNAKprod, peer)
-# (producer, mutexCLEARprod, peer)
(consumer, bufferOKcons, peer)
(consumer, bufferNAKcons, peer)
-# (consumer, mutexOKcons, peer)
-# (consumer, mutexNAKcons, peer)
-# (consumer, mutexCLEARcons, peer)
-# (mutex, setprod, peer)
-# (mutex, clearprod, peer)
(buffer, putprod, peer)
-
-
-# (mutex, setcons, peer)
-# (mutex, clearcons, peer)
(buffer, getcons, peer)
}
Modified: trunk/examples/producer-consumer.topo
===================================================================
--- trunk/examples/producer-consumer.topo 2010-03-11 18:12:37 UTC (rev 16)
+++ trunk/examples/producer-consumer.topo 2010-03-12 07:35:08 UTC (rev 17)
@@ -3,7 +3,7 @@
counts:
producer 2
-consumer 2
+consumer 2
buffer 1
links:
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-11 18:12:37 UTC (rev 16)
+++ trunk/search.scm 2010-03-12 07:35:08 UTC (rev 17)
@@ -40,6 +40,8 @@
;; 1E model as labeled-transition directed graph
(define oneE (void))
+
+
;; the expand function
;;
;; returns all possible new states
@@ -222,7 +224,9 @@
(display-ln "dumping (did NOT really find simulation)")
(values #t result)))
(result
- (values #t (search->model result)))
+ (begin
+ (display-ln "We are going to search now")
+ (values #t (search->model result))))
; otherwise just return failure
(#t
(values #f max-trace))))))))
@@ -591,25 +595,28 @@
;; (using tau transitions)
(define connect-taus!
(lambda (start-state end-state db)
+ ;We want to check if, after going through all tau-transitions from start-state to children
+ ;if we are going to reach the end-state
; dummy check
- (if (equal? start-state end-state) (void)
+ (if (equal? start-state end-state) (begin (display-ln "Start is equal to end \n\n") (void))
(let* ([end-db (make-hash)]
+ [output (if (>= debug 4) (display-ln "Start is "start-state " and end is "end-state "\n") (void))]
[dmy (hash-set! end-db (state->representative end-state) #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
- [success? (ormap (lambda (x) (connect-taus-rec x end-db db)) possibles)])
+ [success? (ormap (lambda (x) (connect-taus-rec x end-db db (make-hash))) possibles)])
(if (not success?) (error "there is a bug in search!") (void))))))
-; returns a list or #f: #f on failure or (list todo final-state)
+; returns a list or #f: #f on failure or (list todo final-state)
; the todo which started this level and the final edge state
; (we need to return the first state of final-todo)
(define connect-taus-rec
- (lambda (init-td final-db db)
+ (lambda (init-td final-db db visited)
(let* ([start-state (todo-state init-td)]
[end-state (todo->next-state init-td)]
- [dmy0 (if (>= debug 4) (display-ln "ctr call:\n\tss: " start-state "\n\tes: " end-state) (void))])
+ [dmy0 (if (>= debug 4) (display-ln "ctr call:\n\tss: " start-state "\n\tes: " end-state"\n\n\n") (void))])
(if (hash-has-key? final-db end-state)
(begin
(if (>= debug 4) (display-ln "found connection in connect-taus-rec!") (void))
@@ -621,12 +628,22 @@
(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)])
+ (let ([res (ormap
+ (lambda (x)
+ (if (hash-has-key? visited (todo-state x))
+ (begin
+ ;(display-ln "visited before" (todo-state x)"\n")
+ ;the state was visited before so no need to try its sub-tau transitions
+ #t)
+ (begin
+ (hash-set! visited end-state #f)
+ (connect-taus-rec x final-db db visited))))
+ possibles)])
; if one of our children found the solution, add its transition and return
(if res
(begin
(add-td-to-db! init-td db) #t)
- #f))))))))
+ #f))))))))
; =============================== partial order reduction =================================== ;
(define ring-reducer-init-big
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-03-11 18:12:47
|
Revision: 16
http://golok.svn.sourceforge.net/golok/?rev=16&view=rev
Author: sralmai
Date: 2010-03-11 18:12:37 +0000 (Thu, 11 Mar 2010)
Log Message:
-----------
[MINOR ENHANCEMENT]: --dump now returns full model if depth is > model size or if depth is -1. Example: --dump -1 builds the first system and returns it.
Modified Paths:
--------------
trunk/search.scm
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-10 21:08:55 UTC (rev 15)
+++ trunk/search.scm 2010-03-11 18:12:37 UTC (rev 16)
@@ -276,8 +276,10 @@
[gr (if new-fringe (hash-map new-fringe (lambda (x y) x)) #f)]
[dbg-dummy (if (>= debug 2) (display-ln "\tdepth " depth " fringe has " (if gr (length gr) 0)) (void))])
- (if (not gr) #f ; there are no more states to search
+ (cond ((and (not gr) (not dump)) #f) ; there are no more states to search
+ ((and (not gr) dump) (make-model (hash->model state-space lt topo-ht start-state state->representative) lt))
+ (#t
; check if some fringe node is the start of 1e simulating chunk
(let ([sim (ormap search-node gr)])
(cond
@@ -289,7 +291,7 @@
(make-model (hash->model state-space lt topo-ht start-state state->representative) lt))
; otherwise, keep going
(#t
- (search-bfs-rec (add1 depth) new-fringe (if dump (sub1 dump) #f)))))))))
+ (search-bfs-rec (add1 depth) new-fringe (if dump (sub1 dump) #f))))))))))
; create a state space and fringe
(define create-sp-and-fr
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-03-10 21:09:02
|
Revision: 15
http://golok.svn.sourceforge.net/golok/?rev=15&view=rev
Author: sralmai
Date: 2010-03-10 21:08:55 +0000 (Wed, 10 Mar 2010)
Log Message:
-----------
[BUGFIX]: added --disable-pruning flag for testing and fixed system output label mangling
Modified Paths:
--------------
trunk/find-k.scm
trunk/golok.scm
trunk/search.scm
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-03-10 19:54:16 UTC (rev 14)
+++ trunk/find-k.scm 2010-03-10 21:08:55 UTC (rev 15)
@@ -72,6 +72,8 @@
(define stop-depth #f)
+ (define pruning #t)
+
; dump depth
(define dump #f)
@@ -99,7 +101,8 @@
(set! process-type (list-ref arg-list 9))
(set! star (list-ref arg-list 10))
(set! dump (list-ref arg-list 11))
- (set! npp (list-ref arg-list 12)))))
+ (set! npp (list-ref arg-list 12))
+ (set! pruning (list-ref arg-list 13)))))
;;; internals ;;;
@@ -190,7 +193,7 @@
; (void))
(dump-sys
(model2dot (find-solution (item-index (automaton-proc-type x) processes) x)
- (string-append output-directory "/" (symbol->string proc-type) "-sys.dot") proc-mask))
+ (string-append output-directory "/" (symbol->string proc-type) "-sys.dot") npp))
(#t
(find-solution (item-index (automaton-proc-type x) processes) x)))))
eps-auts))
@@ -218,6 +221,7 @@
(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
+ #:pruning pruning
#:npp npp
#:ring ring
#:dump dump
@@ -259,6 +263,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
+ #:pruning pruning
#:npp npp
#:ring ring
#:star star
Modified: trunk/golok.scm
===================================================================
--- trunk/golok.scm 2010-03-10 19:54:16 UTC (rev 14)
+++ trunk/golok.scm 2010-03-10 21:08:55 UTC (rev 15)
@@ -57,6 +57,10 @@
; name of process type to check
(define process-type #f)
+
+ ; branch pruning
+ (define pruning #t)
+
; command line parser which sets up environment
(define amf-file
(command-line
@@ -85,7 +89,8 @@
[("-f" "--start-depth") x "Depth to begin searching for simulation" (set! start-depth (string->number x))]
[("-s" "--stop-depth") x "Depth to halt simulation search" (set! stop-depth (string->number x))]
[("-p" "--process-type") x "Search only for a specific process" (set! process-type (string->symbol x))]
+ [("--disable-pruning") "for testing only" (set! pruning #f)]
#:args (amf-file) amf-file ))
-(find-k amf-file (list debug max-t dump-1E dump-sys output-directory dfs ring start-depth stop-depth process-type star dump npp))
+(find-k amf-file (list debug max-t dump-1E dump-sys output-directory dfs ring start-depth stop-depth process-type star dump npp pruning))
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-10 19:54:16 UTC (rev 14)
+++ trunk/search.scm 2010-03-10 21:08:55 UTC (rev 15)
@@ -68,9 +68,6 @@
;; (state? hash-map?) -> (state?)
(define state->representative (void))
-;; for cutting branches
-(define prune-branches? #f)
-
;; hash-map of states already checked for simulation (keys: system-states, values: #t)
(define state-space #f)
@@ -97,6 +94,9 @@
(define debug 2)
+; filter for branch pruning
+(define start-state-filter (void))
+
; print optimizations debugging output
(define opt-dbg 0)
@@ -122,6 +122,7 @@
; start - integer-depth | #f
; stop - integer-depth | #f
(lambda (prot topo pt dfs oneE-start-aut
+ #:pruning [pr #t]
#:npp [npp (list)]
#:dump [dump #f]
#:ring [r #f]
@@ -134,11 +135,10 @@
; 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)
+ ; enable/disable pruning
+ (set! start-state-filter (if pr start-aut-filter (lambda (x) #t)))
+
; TODO: generalize these reductions (and maybe figure them out from the topology)
(cond
((and r (not (null? s)))
@@ -303,15 +303,9 @@
; filter returns true only for systems states which may contain a proc-type process
; in its initial state
-;
-; TODO: need to initialize this... in order to do this, we need to figure out
-; if the process type we are checking has a unique start state
-; (that cannot be revisited)
-(define start-state-filter
+(define start-aut-filter
(lambda (a)
- (if prune-branches? (ormap (lambda (x)
- (= start-aut (mprocess-state x)))
- a) #t)))
+ (ormap (lambda (x) (= start-aut (mprocess-state x))) a)))
(define get-fringe
(lambda (depth state-space fringe)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
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.
|
|
From: <sr...@us...> - 2010-03-09 05:10:25
|
Revision: 13
http://golok.svn.sourceforge.net/golok/?rev=13&view=rev
Author: sralmai
Date: 2010-03-09 05:10:18 +0000 (Tue, 09 Mar 2010)
Log Message:
-----------
[IMPLEMENTATION CHANGE]: 1e composition is no longer projected. SpinLock is now broken, because with only 1 object, simulation of the fully composed 1e never happens. (But SpinLock-mult works fine.)
Modified Paths:
--------------
trunk/examples/SpinLock.amf
trunk/examples/SpinLock.topo
trunk/examples/dme-mult.amf
trunk/find-k.scm
trunk/golok.scm
trunk/model-builder.scm
trunk/run-all.sh
trunk/search.scm
Added Paths:
-----------
trunk/examples/SpinLock-mult.amf
trunk/examples/SpinLock-mult.topo
trunk/examples/producer-consumer.amf
trunk/examples/producer-consumer.topo
Added: trunk/examples/SpinLock-mult.amf
===================================================================
--- trunk/examples/SpinLock-mult.amf (rev 0)
+++ trunk/examples/SpinLock-mult.amf 2010-03-09 05:10:18 UTC (rev 13)
@@ -0,0 +1,54 @@
+#
+# SpinLock.amf
+#
+# automata file for Spin Lock
+#
+# David Samuelson
+# August 4, 2009
+#
+
+process thread {
+START: [initial, epsilon ] -> [ Start, begin ]
+REQUEST: [ Start, begin ] -> [Waiting, req ]
+REJECTED: [Waiting, nack ] -> [Waiting, req ]
+ACCEPTED: [Waiting, ack ] -> [Has_Object, in ]
+RELEASING: [Has_Object, in ] -> [Start, rel ]
+
+}
+
+process object {
+REQ_FREE: [NB, req ] -> [ B, ack ]
+REQ_BUSY: [B, req ] -> [ B, nack]
+RCV_REL: [B, rel ] -> [NB, begin]
+
+}
+
+addition-rule add-thread {
+ create: thread x
+ foreach object y
+ {
+ add: var x -- var y
+ }
+}
+
+addition-rule add-object {
+ create: object x
+ foreach thread y {
+ add: var x -- var y
+ }
+}
+
+topology {
+ (object, req, peer)
+ (object, rel, peer)
+ (thread, in, self)
+ (thread, ack, peer)
+ (thread, nack, peer)
+ (thread, begin, peer)
+ (thread, begin, self)
+}
+
+initial-config {
+}
+
+kernel = SpinLock-mult.topo
Added: trunk/examples/SpinLock-mult.topo
===================================================================
--- trunk/examples/SpinLock-mult.topo (rev 0)
+++ trunk/examples/SpinLock-mult.topo 2010-03-09 05:10:18 UTC (rev 13)
@@ -0,0 +1,12 @@
+model: SpinLock.amf
+
+counts:
+thread 2
+object 2
+
+links:
+
+thread 0 -- object 0
+thread 0 -- object 1
+thread 1 -- object 0
+thread 1 -- object 1
Modified: trunk/examples/SpinLock.amf
===================================================================
--- trunk/examples/SpinLock.amf 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/examples/SpinLock.amf 2010-03-09 05:10:18 UTC (rev 13)
@@ -1,11 +1,8 @@
#
# SpinLock.amf
#
-# automata file for Spin Lock
+# behavioral automata for spinlock
#
-# David Samuelson
-# August 4, 2009
-#
process thread {
START: [initial, epsilon ] -> [ Start, begin ]
@@ -23,6 +20,7 @@
}
+
addition-rule add-thread {
create: thread x
foreach object y
@@ -31,13 +29,6 @@
}
}
-addition-rule add-object {
- create: object x
- foreach thread y {
- add: var x -- var y
- }
-}
-
topology {
(object, req, peer)
(object, rel, peer)
@@ -47,7 +38,6 @@
(thread, begin, peer)
(thread, begin, self)
}
-
initial-config {
}
Modified: trunk/examples/SpinLock.topo
===================================================================
--- trunk/examples/SpinLock.topo 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/examples/SpinLock.topo 2010-03-09 05:10:18 UTC (rev 13)
@@ -2,11 +2,9 @@
counts:
thread 2
-object 2
+object 1
links:
thread 0 -- object 0
-thread 0 -- object 1
thread 1 -- object 0
-thread 1 -- object 1
Modified: trunk/examples/dme-mult.amf
===================================================================
--- trunk/examples/dme-mult.amf 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/examples/dme-mult.amf 2010-03-09 05:10:18 UTC (rev 13)
@@ -6,12 +6,12 @@
#
#
process forward {
-IDLE: [ Idle, token] -> [ Idle, token]
-SND: [Start, epsilon] -> [Idle, token]
+IDLE: [ Idle, token] -> [ Idle, token2]
+SND: [Start, epsilon] -> [Idle, token2]
}
process critical {
-ENTER: [ Idle, token ] -> [ Cs , in ]
+ENTER: [ Idle, token2 ] -> [ Cs , in ]
LEAVE: [ Cs , in ] -> [ Idle , token ]
}
@@ -31,7 +31,7 @@
}
topology {
- ( critical, token, lpeer)
+ ( critical, token2, lpeer)
( critical, in, self)
( forward, token, lpeer)
}
Added: trunk/examples/producer-consumer.amf
===================================================================
--- trunk/examples/producer-consumer.amf (rev 0)
+++ trunk/examples/producer-consumer.amf 2010-03-09 05:10:18 UTC (rev 13)
@@ -0,0 +1,81 @@
+process producer {
+
+init: [Init, epsilon] -> [Produced, item]
+produced: [Produced, item] -> [AddBuffer, putprod]
+#recvnak: [WaitMutex, mutexNAKprod] -> [WaitMutex, setprod]
+#recvok: [WaitMutex, mutexOKprod] -> [AddBuffer, putprod]
+addbuffernak: [AddBuffer, bufferNAKprod] -> [AddBuffer, putprod]
+addbufferok: [AddBuffer, bufferOKprod] -> [Produced, item]
+#recvmutexok: [ClearMutex, mutexCLEARprod] -> [Produced, item]
+}
+
+process consumer {
+init2: [Init2, epsilon] -> [GetBuffer, getcons]
+#recvnak2: [WaitMutex, mutexNAKcons] -> [WaitMutex, setcons]
+#recvok2: [WaitMutex, mutexOKcons] -> [GetBuffer, getcons]
+getnak2: [GetBuffer, bufferNAKcons] -> [GetBuffer, getcons]
+getok2: [GetBuffer, bufferOKcons] -> [GetBuffer, getcons]
+#recvreplay: [ClearMutex, mutexCLEARcons] -> [GetBuffer, getcons]
+}
+
+# process mutex {
+# setpassprod: [Clear, setprod] -> [Set, mutexOKprod]
+# setfailprod: [Set, setprod] -> [Set, mutexNAKprod]
+# clearprod: [Set, clearprod] -> [Clear, mutexCLEARprod]
+
+# setpasscons: [Clear, setcons] -> [Set, mutexOKcons]
+# setfailcons: [Set, setcons] -> [Set, mutexNAKcons]
+# clearcons: [Set, clearcons] -> [Clear, mutexCLEARcons]
+# }
+
+
+process buffer {
+ putzeroprod: [Zero, putprod] -> [One, bufferOKprod]
+
+ putoneprod: [One, putprod] -> [One, bufferNAKprod]
+
+ getzerocons: [Zero, getcons] -> [Zero, bufferNAKcons]
+
+ getonecons: [One, getcons] -> [Zero, bufferOKcons]
+
+}
+
+addition-rule add-producer {
+ create: producer x
+# add: var x -- mutex 0
+ add: var x -- buffer 0
+}
+
+addition-rule add-consumer {
+ create: consumer x
+# add: var x -- mutex 0
+ add: var x -- buffer 0
+}
+
+topology {
+ (producer, item, self)
+ (producer, bufferOKprod, peer)
+ (producer, bufferNAKprod, peer)
+# (producer, mutexOKprod, peer)
+# (producer, mutexNAKprod, peer)
+# (producer, mutexCLEARprod, peer)
+ (consumer, bufferOKcons, peer)
+ (consumer, bufferNAKcons, peer)
+# (consumer, mutexOKcons, peer)
+# (consumer, mutexNAKcons, peer)
+# (consumer, mutexCLEARcons, peer)
+
+# (mutex, setprod, peer)
+# (mutex, clearprod, peer)
+ (buffer, putprod, peer)
+
+
+# (mutex, setcons, peer)
+# (mutex, clearcons, peer)
+ (buffer, getcons, peer)
+}
+
+initial-config {
+}
+
+kernel = producer-consumer.topo
Added: trunk/examples/producer-consumer.topo
===================================================================
--- trunk/examples/producer-consumer.topo (rev 0)
+++ trunk/examples/producer-consumer.topo 2010-03-09 05:10:18 UTC (rev 13)
@@ -0,0 +1,15 @@
+model: producer-consumer.amf
+
+counts:
+
+producer 2
+consumer 2
+buffer 1
+
+links:
+
+producer 0 -- buffer 0
+producer 1 -- buffer 0
+
+consumer 0 -- buffer 0
+consumer 1 -- buffer 0
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/find-k.scm 2010-03-09 05:10:18 UTC (rev 13)
@@ -75,6 +75,14 @@
; dump depth
(define dump #f)
+ ; list of non-paramterized process names
+ (define npp (list))
+
+;; TODO: figure out if there is any better way for
+;; passing arguments across modules
+;; (while avoiding circular "requires")
+;; because this is ugly as sin
+;;
;; set globals passed via command line arguments
(define init-clo
(lambda (arg-list)
@@ -90,7 +98,8 @@
(set! stop-depth (list-ref arg-list 8))
(set! process-type (list-ref arg-list 9))
(set! star (list-ref arg-list 10))
- (set! dump (list-ref arg-list 11)))))
+ (set! dump (list-ref arg-list 11))
+ (set! npp (list-ref arg-list 12)))))
;;; internals ;;;
@@ -156,33 +165,34 @@
[starts (if process-type
(let* ([names (protocol-process-names prot)]
[index (item-index process-type names)])
- (if (< index 0) (raise-user-error "Invalid process index ~s" process-type)
+ (cond
+ ((< index 0) (raise-user-error "Invalid process index ~s" process-type))
+ (#t
(begin
(display-ln "INFO: only checking " process-type " for simulation\n")
- (list index))))
+ (list index)))))
; otherwise, check all process indices
(build-list (length (protocol-process-names prot)) values))])
- (for-each
- (lambda (start-aut)
+ ;;
+ ;; TODO: clean this up... should
+ ;;
(for-each
(lambda (x)
(let* ([processes (protocol-process-names prot)]
- [proc-type (list-ref processes x)]
+ [proc-type (automaton-proc-type x)]
[proc-mask (remove proc-type processes)])
(cond
+ ; if this is a non-parameterized process type, skip
+ ((member (automaton-proc-type x) npp) (void))
; 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))
+ ; ((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))
+ (model2dot (find-solution (item-index (automaton-proc-type x) processes) x)
+ (string-append output-directory "/" (symbol->string proc-type) "-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))
+ (find-solution (item-index (automaton-proc-type x) processes) x)))))
eps-auts))
(dump-solution))))
@@ -206,8 +216,7 @@
[mask (remove name names)])
(let-values ([(tt oneE-builder) (build-oneEmodel-builder prot)])
(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))])
+ (string-append output-directory "/" (symbol->string name) "-1e.dot") #:show-buf #f) (void))])
(let-values ([(soln data) (search prot k name dfs start-aut
#:ring ring
#:dump dump
Modified: trunk/golok.scm
===================================================================
--- trunk/golok.scm 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/golok.scm 2010-03-09 05:10:18 UTC (rev 13)
@@ -8,7 +8,7 @@
(require scheme/cmdline)
;; version header -- should be in form vx.y.z(-tag)
- (define version "v0.1.3.0")
+ (define version "v0.1.4.0")
; parsed values of command line arguments
; currently size 11
@@ -33,9 +33,13 @@
; ring partial order reduction
(define ring #f)
- ; start partial order reduction
+ ; star partial order reduction
(define star (list))
+ ; non-parameterized processes
+ ; TODO: should be able to discover this from addition rules
+ (define npp (list))
+
; just dump the model at a particular depth
(define dump #f)
@@ -50,9 +54,9 @@
; TODO: not implemented
(define stop-depth #f)
- ; index of process type to check
+ ; name of process type to check
(define process-type #f)
-
+
; command line parser which sets up environment
(define amf-file
(command-line
@@ -60,6 +64,7 @@
#:multi
[("--star-point") x "partial order reduction for star" (set! star (cons (string->symbol x) star))]
+ [("--npp" "--non-parameterized-process") x "do not check process type for simulation" (set! npp (cons (string->symbol x) npp))]
#:once-each
[("-t" "--max-time") num "Specify a maximum execution time in seconds before stopping"
@@ -79,8 +84,8 @@
[("--ring") "assume system states are equivalent under rotation" (set! ring #t)]
[("-f" "--start-depth") x "Depth to begin searching for simulation" (set! start-depth (string->number x))]
[("-s" "--stop-depth") x "Depth to halt simulation search" (set! stop-depth (string->number x))]
- [("-p" "--process-type") x "Search only for a specific process" (set! process-type (string->number x))]
+ [("-p" "--process-type") x "Search only for a specific process" (set! process-type (string->symbol x))]
#:args (amf-file) amf-file ))
-(find-k amf-file (list debug max-t dump-1E dump-sys output-directory dfs ring start-depth stop-depth process-type star dump))
+(find-k amf-file (list debug max-t dump-1E dump-sys output-directory dfs ring start-depth stop-depth process-type star dump npp))
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/model-builder.scm 2010-03-09 05:10:18 UTC (rev 13)
@@ -149,7 +149,7 @@
[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)]
+ [stripped (strip-taus-short model (proc->proc-id proc-type tt) tt)]
;; remove all duplicate paths
[cleaned-model (reduce-model stripped)]
;; remove lonely nodes (without transitions to or from)
Modified: trunk/run-all.sh
===================================================================
--- trunk/run-all.sh 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/run-all.sh 2010-03-09 05:10:18 UTC (rev 13)
@@ -2,7 +2,7 @@
# this *should* be something nice to ensure stuff works
-TESTS="dme dme-mult SpinLock"
+TESTS="dme dme-mult SpinLock-mult dpp lr-dpp"
make clean
make
@@ -17,12 +17,20 @@
for i in $TESTS
do
echo "Testing BFS"
+ if [[ "$i" == "SpinLock" ]]
+ then
+ ./golok -o output --npp object examples/$i.amf || fail
+ elif [[ "$i" == "producer-consumer" ]]
+ then
+ ./golok -o output --npp buffer examples/$i.amf || fail
+ else
./golok -o output examples/$i.amf || fail
+ fi
make clean
-echo "Testing DFS"
- ./golok -o output --dfs examples/$i.amf || fail
- make clean
+##echo "Testing DFS"
+ # ./golok -o output --dfs examples/$i.amf || fail
+# make clean
done
make clean
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-03-05 05:40:56 UTC (rev 12)
+++ trunk/search.scm 2010-03-09 05:10:18 UTC (rev 13)
@@ -137,7 +137,7 @@
(set! state->representative (ring-reducer-init (length (protocol-process-names prot))))))
((not (null? s))
(begin
- (display-ln "INFO: enabling start partial order reduction on " (los->string s))
+ (display-ln "INFO: enabling star partial order reduction on " (los->string s))
(set! state->representative (star-reducer-init ss s lookup-table))))
(#t
(set! state->representative (lambda (x . y) x))))
@@ -378,10 +378,11 @@
(#t
; otherwise, expand all possible branches
; first collect all states reachable via tau transitions
- (let* ([starts (explode state (list proc-type-id))]
+ (let* ([starts (list state)];(explode state (list proc-type-id))]
; 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 other-mask-ids #t)) starts))]
+ (list-of-lists->list (map (lambda (x) (expand x (list) #t)) starts))]
; finally sort the transitions according to the needed 1e transitions
[check-list (condense possibles index)])
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
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.
|
|
From: <sr...@us...> - 2010-03-02 05:32:22
|
Revision: 11
http://golok.svn.sourceforge.net/golok/?rev=11&view=rev
Author: sralmai
Date: 2010-03-02 05:32:14 +0000 (Tue, 02 Mar 2010)
Log Message:
-----------
[IMPLEMENTATION CHANGE]: removed "as perspective" 1e models from testing. So only processes with an epsilon transition are tested for simulation, and each has a single 1e model constructed via composition from that start transition. (Tested with dme, dme-mult, SpinLock, and lr-dpp.)
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 01:26:24 UTC (rev 10)
+++ trunk/find-k.scm 2010-03-02 05:32:14 UTC (rev 11)
@@ -151,34 +151,36 @@
(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 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))))
+ (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* ([names (protocol-process-names prot)]
[index (item-index process-type names)])
- (if (< index 0) (raise-user-error "Invalid process index ~s" process-type)
+ (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
(begin
(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))))
-
- ;; collect all automata which take an epsilon in message
- (filter (lambda (z) (equal? eps (automaton-in-msg z))) (protocol-ba prot)))
-
+ (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)))))
(dump-solution))))
(define dump-solution
@@ -194,15 +196,14 @@
;; TODO: clean up find-solution and find-solution-rec
(define find-solution
- (lambda (id start-aut)
+ (lambda (id)
(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 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
+ (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
#:ring ring
#:dump dump
#:star star
@@ -211,7 +212,7 @@
(if soln
; if soln == #t, then data is a model containing the simulating subset of the system
data
- (find-solution-rec id start-aut names 0 data))))))))
+ (find-solution-rec id names 0 data))))))))
;; if we try all addition rules and none work, which rule should be applied before looping over them again
@@ -230,7 +231,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 start-aut names cur_ch best-trace)
+ (lambda (id names cur_ch best-trace)
(let* ([rules (protocol-addition-rules prot)]
[rule (list-ref (protocol-addition-rules prot) cur_ch)]
[size (length rules)]
@@ -242,7 +243,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 start-aut
+ (let-values ([(soln data) (search prot new-k (list-ref names id) dfs
#:ring ring
#:star star
#:start start-depth
@@ -258,7 +259,7 @@
(begin
(set! k new-k)
(set! made-a-change #t)
- (find-solution-rec id start-aut names (modulo (+ 1 cur_ch) size) data)))
+ (find-solution-rec id names (modulo (+ 1 cur_ch) size) data)))
; is the the last rule before trying them all again?
((= 0 (modulo (+ 1 cur_ch) size))
@@ -267,17 +268,17 @@
; clear the flag and continue
(begin
(set! made-a-change #f)
- (find-solution-rec id start-aut names (modulo (+ 1 cur_ch) size) best-trace))
+ (find-solution-rec id 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 start-aut names (modulo (+ 1 cur_ch) size) best-trace))))
+ (find-solution-rec id names (modulo (+ 1 cur_ch) size) best-trace))))
; otherwise just continue to the next rule
- (#t (find-solution-rec id start-aut names (modulo (+ 1 cur_ch) size) best-trace)))))))))
+ (#t (find-solution-rec id names (modulo (+ 1 cur_ch) size) best-trace)))))))))
; depreciated
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-03-01 01:26:24 UTC (rev 10)
+++ trunk/model-builder.scm 2010-03-02 05:32:14 UTC (rev 11)
@@ -131,53 +131,28 @@
(let ([tt (create-lookup-table (protocol-ba prot) #t)])
(values
tt
- (lambda (proc-type initial-aut [verbose #f])
+ (lambda (proc-type [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))]
- ; [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))))]
+ [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))))]
[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)
+ [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)))]
[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)]
- ;; 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)))))))
+ [cleaned-model (reduce-model stripped)])
+ (make-model cleaned-model 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 01:26:24 UTC (rev 10)
+++ trunk/search.scm 2010-03-02 05:32:14 UTC (rev 11)
@@ -115,8 +115,7 @@
; 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 oneE-start-aut
- #:dump [dump #f]
+ (lambda (prot topo pt dfs #:dump [dump #f]
#:ring [r #f]
#:star [s (list)]
#:start [start-d #f]
@@ -186,7 +185,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))))
; 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.
|
|
From: <sr...@us...> - 2010-03-01 01:35:41
|
Revision: 9
http://golok.svn.sourceforge.net/golok/?rev=9&view=rev
Author: sralmai
Date: 2010-03-01 00:44:47 +0000 (Mon, 01 Mar 2010)
Log Message:
-----------
[NEW FEATURE]: "star" reduction implemented (for each process type whose processes are interchangable, use a "--star-point <process type>" flag) (tested with SpinLock... it finds the same cutoff, but the path in the system model is actually longer (because there are multiple simulating pathways). In any event, it works)
Modified Paths:
--------------
trunk/examples/milners.amf
trunk/golok.scm
trunk/search.scm
Modified: trunk/examples/milners.amf
===================================================================
--- trunk/examples/milners.amf 2010-02-24 05:58:43 UTC (rev 8)
+++ trunk/examples/milners.amf 2010-03-01 00:44:47 UTC (rev 9)
@@ -11,12 +11,14 @@
INIT: [Start, epsilon] -> [begin, token]
# Receive token before computation
-WAIT_TKN: [task-run, token] -> [task-wtoken, compute]
-WAIT_TSK: [task-wtoken, compute]-> [begin, token]
+WAIT_TKN: [task-run, token] -> [task-wtoken, send-token]
+# and send the token
+WAIT_TSK_START: [send-token, send-token ] -> [task-run, token ]
+
# Finish task before receiving token
-TASK_DONE: [task-run, compute] -> [wait-token, token]
-RESTART: [wait-token, token] -> [begin, token]
+TASK_DONE: [task-run, compute] -> [wait-token, compute]
+RESTART: [wait-token, token] -> [task-run, token]
}
@@ -29,8 +31,9 @@
}
topology {
- (scheduler,token,peer)
+ (scheduler,token,lpeer)
(scheduler,compute,self)
+ (scheduler,send-token,self)
}
initial-config{
Modified: trunk/golok.scm
===================================================================
--- trunk/golok.scm 2010-02-24 05:58:43 UTC (rev 8)
+++ trunk/golok.scm 2010-03-01 00:44:47 UTC (rev 9)
@@ -59,7 +59,7 @@
#:program (string-append "golok" "-" version)
#:multi
- [("--star-point") x "partial order reduction for star" (cons (string->symbol x) star)]
+ [("--star-point") x "partial order reduction for star" (set! star (cons (string->symbol x) star))]
#:once-each
[("-t" "--max-time") num "Specify a maximum execution time in seconds before stopping"
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-02-24 05:58:43 UTC (rev 8)
+++ trunk/search.scm 2010-03-01 00:44:47 UTC (rev 9)
@@ -1,4 +1,3 @@
-
; search.scm
;
; Algorithm for checking a system instance for
@@ -137,10 +136,10 @@
(set! state->representative (ring-reducer-init (length (protocol-process-names prot))))))
((not (null? s))
(begin
- (display-ln "STUB: partial order reduction not implemented")
- (set! state->representative (lambda (x . y) x))))
+ (display-ln "INFO: enabling start partial order reduction on " (los->string s))
+ (set! state->representative (star-reducer-init ss s lookup-table))))
(#t
- (set! state->representative (lambda (x . y) x))))
+ (set! state->representative (lambda (x . y) x))))
; set a bunch of global (to this module) variables
@@ -180,7 +179,7 @@
(filter (lambda (x) (equal? proc-type (process-name x)))
(protocol-processes prot)))))) lt))
- (set! other-mask (remove proc-type (protocol-process-names prot))))
+ (set! other-mask (remove proc-type (protocol-process-names prot)))
(set! proc-type-id (proc->proc-id proc-type lt))
(set! other-mask-ids (map (lambda (x) (proc->proc-id x lt)) other-mask))
@@ -210,7 +209,7 @@
(values #t (search->model result)))
; otherwise just return failure
(#t
- (values #f max-trace)))))))
+ (values #f max-trace))))))))
(define search-dfs
(lambda (state)
@@ -546,9 +545,9 @@
; if start-state does not equal the initial state of the proc-type transition,
; then at least one tau transition needed to happen, first
(begin
- (if (not (equal? start-state (state->representative (todo-state td))))
- (connect-taus! start-state (state->representative (todo-state td)) db)
- (void))
+ (if (not (equal? start-state (todo-state td)))
+ (connect-taus! start-state (todo-state td) db)
+ (void))
(add-td-to-db! td db)))) (cadr entry)))))
(define add-td-to-db!
@@ -588,7 +587,6 @@
;
; if it *does* return false, there is an error in our search algorithm
[success? (ormap (lambda (x) (connect-taus-rec x end-db db)) possibles)])
-
(if (not success?) (error "there is a bug in search!") (void))))))
; returns a list or #f: #f on failure or (list todo final-state)
@@ -654,45 +652,96 @@
(lambda (x . y)
(car (sort (all-rotations x sz) order-by-number)))))
-; x, y are system states
;
+;
+;
+;
+(define star-reducer-init
+ (lambda (example-state reducible-elements lt)
+ (let* ([reducible-ids (map (lambda (x) (proc->proc-id x lt)) reducible-elements)]
+ ; chunks is a list of pairs (integer? integer?)
+ ; where (a b)
+ ; means starting at a, b elements can be sorted
+ ; (in other words, the sublist of length b starting at a
+ ; can be chopped out of the full list, sorted, and put back in)
+ [chunks (map (lambda (x) (list (find-first-rec x example-state 0) (count-number x example-state)))
+ reducible-ids)])
+ (lambda (z . y)
+ (reduce-chunks z chunks)))))
+
+(define reduce-chunks
+ (lambda (x chunks)
+ (if (null? chunks) x
+ (let ([start-index (caar chunks)]
+ [len (cadar chunks)])
+ (let-values ([(front mid) (split-at x start-index)])
+ (let-values ([(to-sort back) (split-at mid len)])
+ (reduce-chunks (append front (sort to-sort sort-mprocess) back) (cdr chunks))))))))
+
+;
+; return the first index of the list in which the process-type (parameter integer?) matches (car mprocess)
+; (integer? (list-of mprocess?)) -> (integer?)
+;
+(define find-first-rec
+ (lambda (id ls index)
+ (if (= id (state-id->proc-id (mprocess-state (car ls))))
+ index
+ (find-first-rec id (cdr ls) (add1 index)))))
+
+;
+; return the number of processes in the state of process type id
+;
+(define count-number
+ (lambda (id st)
+ (length (filter (lambda (x) (= id (state-id->proc-id (mprocess-state x)))) st))))
+
+(define (sort-mprocess x y)
+ (if (> (sort-mprocess-raw x y) 0) #f #t))
+;
+; returns -1, 0, or 1
+; based on ordering of xs1 and ys1
+; (-1 means xs1 < ys1, 0 : xs1 = ys1, 1 :xs1 > ys1)
+(define (sort-mprocess-raw xs1 ys1)
+ (let ([xs1-id (mprocess-state xs1)]
+ [ys1-id (mprocess-state ys1)])
+ (cond
+ ((< xs1-id ys1-id) -1)
+ ((> xs1-id ys1-id) 1)
+ ;; states are equal, so compare buffers
+ (#t
+ (let* ([xbuf (mprocess-buff xs1)]
+ [ybuf (mprocess-buff ys1)]
+ [xlen (length xbuf)]
+ [ylen (length ybuf)])
+ (cond
+ ((< xlen ylen) -1)
+ ((> xlen ylen) 1)
+ ((equal? xbuf ybuf) 0)
+ ((which-is-first? xbuf ybuf))))))))
+
+; x, y are system states (that is, a list of mprocess structs)
+;
; returns true if x is "less than" y
(define (order-by-number x y)
; if x and y were completely equal, just say x is first
(if (or (null? x) (null? y)) #t
- (let ([xs1 (mprocess-state (car x))]
- [ys1 (mprocess-state (car y))])
- (cond
- ((< xs1 ys1) #t)
- ((> xs1 ys1) #f)
- ;; states are equal, so compare buffers
- (#t
- (let* ([xbuf (mprocess-buff (car x))]
- [ybuf (mprocess-buff (car y))]
- [xlen (length xbuf)]
- [ylen (length ybuf)])
- (cond
- ((< xlen ylen) #t)
- ((> xlen ylen) #f)
- ;; if message buffers are equal, give up and check the next process
- ((equal? xbuf ybuf)
- (order-by-number (cdr x) (cdr y)))
- ;; otherwise, the "lower" messages go first
- (#t
- (which-is-first? xbuf ybuf)))))))))
+ (let ([res (sort-mprocess-raw (car x) (car y))])
+ (cond
+ ((= res -1) #t)
+ ((= res 1) #f)
+ (#t (order-by-number (cdr x) (cdr y)))))))
-
; like order-by-number, except for simple lists of integers
;
-; returns true if x < y
+; returns -1 if x < y
;
-; WARNING: this assumes that x != y and len(x) == len(y)
+; WARNING: assumes x and y are non-equal
(define (which-is-first? x y)
(let ([x1 (car x)]
[y1 (car y)])
(cond
- ((< x1 y1) #t)
- ((> x1 y1) #f)
+ ((< x1 y1) -1)
+ ((> x1 y1) 1)
(#t (which-is-first? (cdr x) (cdr y))))))
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
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.
|
|
From: <sr...@us...> - 2010-02-24 05:58:50
|
Revision: 8
http://golok.svn.sourceforge.net/golok/?rev=8&view=rev
Author: sralmai
Date: 2010-02-24 05:58:43 +0000 (Wed, 24 Feb 2010)
Log Message:
-----------
[BUGFIX]: composed 1e models are now correctly compacted (states with only tau outputs are removed after relinking)
Modified Paths:
--------------
trunk/model-builder.scm
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-02-23 22:53:44 UTC (rev 7)
+++ trunk/model-builder.scm 2010-02-24 05:58:43 UTC (rev 8)
@@ -148,7 +148,6 @@
[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
- ; XXX
[stripped (strip-taus model (proc->proc-id proc-type tt) tt)]
[cleaned-model (reduce-model stripped)])
(make-model cleaned-model tt)))))))
@@ -166,7 +165,9 @@
(define (strip-taus raw-model proc-id lt)
(let* ([model (remove-tau-linking raw-model lt)]
- [new-model (make-vector (vector-length model))])
+ [new-model (make-vector (vector-length model))]
+ ; lookups to compacted model (without "extra" start states)
+ [mapper (make-hash)])
(begin
; rebuild the model (leaving out transitions)
(for-each (lambda (x)
@@ -180,43 +181,73 @@
(vector-set! new-model x new-entry))))
(build-list (vector-length new-model) values))
- ; for each state, for each link of type proc-id, point it to the
- ; next state which works
- (for-each
- ; x is state index
- (lambda (x)
- ; trans is a list of all "collapsed" transitions
- (let ([trans (remove-duplicates (collect-endpoints x proc-id model))]
- [new-entry (vector-ref new-model x)])
- ;; put the collapsed transitions in the new model
+ ; for each state reachable via non-tau links, add the map
+ (add-elements-rec 0 proc-id model new-model mapper)
+
+ ;; return the compacted new model
+ (compact-model new-model mapper))))
+
+
+;; shrink a model (remove states and correct indexing) given a model and a map of old indices to new indices
+(define (compact-model model mapper)
+ (let ([new-model (make-vector (hash-count mapper))])
+ (begin
+ (hash-for-each mapper
+ (lambda (x y)
+ (let ([state (vector-ref (vector-ref model x) 0)]
+ [trans (vector-ref (vector-ref model x) 1)]
+ [new-state (make-vector 2)])
+ (begin
+ ;; copy the old state into the new
+ (vector-set! new-state 0 state)
+ ;; change all the next-indices of the transitions
+ ;; add the modified transitions to the state
+ (vector-set! new-state 1 (map (lambda (z)
+ (let ([new-tran (vector-copy z)])
+ (begin
+ (vector-set! new-tran 3 (hash-ref mapper (vector-ref z 3)))
+ new-tran))) trans))
+ ;; write the whole thing into the new model
+ (vector-set! new-model y new-state)))))
+ ; return the new model
+ new-model)))
+
+
+
+
+(define (add-elements-rec index proc-id model new-model mapper)
+ (if (hash-has-key? mapper index) (void)
+ (let* ([trans (remove-duplicates (collect-endpoints index proc-id model))]
+ [new-entry (vector-ref new-model index)]
+ [size (hash-count mapper)])
+ (begin
(vector-set! new-entry 1 trans)
- (vector-set! new-model x new-entry)))
- (build-list (vector-length model) values))
+ (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))
+ trans)))))
- ;; return the model
- new-model)))
-
-
-(define (collect-endpoints start-index proc-id model)
+(define (collect-endpoints state-index proc-id model)
(let ([ends (make-vector 1 (list))]
[visit-list (make-hash)])
(begin
- (collect-endpoints-rec start-index proc-id model ends visit-list)
+ (collect-endpoints-rec state-index proc-id model ends visit-list)
(vector-ref ends 0))))
-(define (collect-endpoints-rec to-ind proc-id model ends visited-list)
- (if (hash-has-key? visited-list to-ind)
+(define (collect-endpoints-rec state-index proc-id 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))))
- (vector-ref (vector-ref model to-ind) 1))]
+ (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)))))
- (vector-ref (vector-ref model to-ind) 1))])
+ (vector-ref (vector-ref model state-index) 1))])
(begin
; mark this index
- (hash-set! visited-list to-ind #t)
+ (hash-set! visited-list state-index #t)
(cond
; if there are no taus from here, just add all these transitions
((null? non-pid-tran)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-02-23 22:54:03
|
Revision: 7
http://golok.svn.sourceforge.net/golok/?rev=7&view=rev
Author: sralmai
Date: 2010-02-23 22:53:44 +0000 (Tue, 23 Feb 2010)
Log Message:
-----------
[BUGFIX]: fixed bug in tau collapsing when constructing composed 1e models (Thanks, Youssef, for hunting this down!)
Modified Paths:
--------------
trunk/model-builder.scm
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-02-23 02:26:41 UTC (rev 6)
+++ trunk/model-builder.scm 2010-02-23 22:53:44 UTC (rev 7)
@@ -185,34 +185,23 @@
(for-each
; x is state index
(lambda (x)
- ; y is a particular transition
- (for-each
- (lambda (y)
- ; ends is a list of indices
- (let ([ends (collect-endpoints (vector-ref y 3) proc-id model)])
- (for-each
- (lambda (z)
- (let* ([new-tran (vector-copy y)]
- [entry (vector-ref new-model x)]
- [old-list (vector-ref entry 1)])
- (begin
- (vector-set! new-tran 3 z)
- (vector-set! entry 1 (cons new-tran old-list))
- (vector-set! new-model x entry))))
- ends)))
- (filter (lambda (a) (= proc-id (state-id->proc-id (vector-ref a 2))))
- (vector-ref (vector-ref model x) 1))))
+ ; trans is a list of all "collapsed" transitions
+ (let ([trans (remove-duplicates (collect-endpoints x proc-id model))]
+ [new-entry (vector-ref new-model x)])
+ ;; put the collapsed transitions in the new model
+ (vector-set! new-entry 1 trans)
+ (vector-set! new-model x new-entry)))
(build-list (vector-length model) values))
;; return the model
new-model)))
-(define (collect-endpoints to-index proc-id model)
+(define (collect-endpoints start-index proc-id model)
(let ([ends (make-vector 1 (list))]
[visit-list (make-hash)])
(begin
- (collect-endpoints-rec to-index proc-id model ends visit-list)
+ (collect-endpoints-rec start-index proc-id model ends visit-list)
(vector-ref ends 0))))
@@ -220,29 +209,28 @@
(if (hash-has-key? visited-list to-ind)
; if we've been here before, die
(void)
- ;; count the out references
- (let* ([pid-out-ids (map (lambda (x) (vector-ref x 3))
- (filter (lambda (y) (= proc-id (state-id->proc-id (vector-ref y 2))))
- (vector-ref (vector-ref model to-ind) 1)))]
- [non-pid-out-ids (map (lambda (x) (vector-ref x 3))
- (filter (lambda (y) (not (= proc-id (state-id->proc-id (vector-ref y 2)))))
- (vector-ref (vector-ref model to-ind) 1)))])
+ ;; count the transitions
+ (let* ([pid-tran (filter (lambda (y) (= proc-id (state-id->proc-id (vector-ref y 2))))
+ (vector-ref (vector-ref model to-ind) 1))]
+ [non-pid-tran (filter (lambda (y) (not (= proc-id (state-id->proc-id (vector-ref y 2)))))
+ (vector-ref (vector-ref model to-ind) 1))])
(begin
; mark this index
(hash-set! visited-list to-ind #t)
(cond
- ; if there are no taus from here, just add the index that got us here and die
- ((null? non-pid-out-ids)
- (vector-set! ends 0 (cons to-ind (vector-ref ends 0))))
- ; if everything is a tau transition, don't add this state, just its children
- ((null? pid-out-ids)
- (for-each (lambda (z) (collect-endpoints-rec z proc-id model ends visited-list)) non-pid-out-ids))
- ; otherwise, add this state and its children
+ ; if there are no taus from here, just add all these transitions
+ ((null? non-pid-tran)
+ (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))
+ (map (lambda (a) (vector-ref a 3)) non-pid-tran)))
+ ; otherwise, add these transitions and their children
(#t
(begin
- (vector-set! ends 0 (cons to-ind (vector-ref ends 0)))
- (for-each (lambda (z)
- (collect-endpoints-rec z proc-id model ends visited-list)) non-pid-out-ids))))))))
+ (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))
+ (map (lambda (a) (vector-ref a 3)) non-pid-tran)))))))))
;;
;; (vector?) -> (vector?)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-02-23 02:26:47
|
Revision: 6
http://golok.svn.sourceforge.net/golok/?rev=6&view=rev
Author: sralmai
Date: 2010-02-23 02:26:41 +0000 (Tue, 23 Feb 2010)
Log Message:
-----------
[BUGFIX]: partial order reduction with --ring fixed (tested with dme.amf and dpp.amf)
Modified Paths:
--------------
trunk/model-builder.scm
trunk/search.scm
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-02-21 02:36:42 UTC (rev 5)
+++ trunk/model-builder.scm 2010-02-23 02:26:41 UTC (rev 6)
@@ -30,9 +30,6 @@
; generation-function: (state [proc-mask (list)] [to-todo #f]) -> (list-of next-states)
init-stepper
- ; struct
- todo-state
-
; todo->label: (todo) -> (label)
todo->label
@@ -616,7 +613,8 @@
(let* ([ss-id (get-id (state->representative (todo-state z) sp) db)]
[to-id (get-id (state->representative (todo->next-state z) sp) db)])
(add-trans-to-set! (todo-state z) (todo->label to-id z) db)))
- (filter (lambda (g) (hash-has-key? db (state->representative (todo->next-state g) sp))) todos)))))
+ (filter (lambda (g) (and (hash-has-key? db (state->representative (todo->next-state g) sp)) (hash-has-key? db (state->representative (todo-state g) sp)))) todos)))))
+
(let ([vect (make-vector (hash-count db))])
(begin
(hash-for-each db (lambda (x y)
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-02-21 02:36:42 UTC (rev 5)
+++ trunk/search.scm 2010-02-23 02:26:41 UTC (rev 6)
@@ -65,6 +65,8 @@
(define unsat (void))
;; function which maps a system state to a specific representative (~ is partial order reduction)
+;;
+;; (state? hash-map?) -> (state?)
(define state->representative (void))
;; for cutting branches
@@ -121,8 +123,6 @@
#:stop [stop-d #f])
(let-values ([(stepper ss lookup-table topo-hash) (init-stepper prot topo)])
(begin
- ; set a bunch of global (to this module) variables
- (set! start-state ss)
; TODO: generalize these reductions (and maybe figure them out from the topology)
(cond
@@ -142,6 +142,10 @@
(#t
(set! state->representative (lambda (x . y) x))))
+
+ ; set a bunch of global (to this module) variables
+ (set! start-state (state->representative ss))
+
; XXX: cleanup
(set! lt lookup-table)
(set! topo-ht topo-hash)
@@ -152,7 +156,25 @@
; TODO: set up branch pruning
- (set! expand stepper)
+ ;;; add wrapper around the expand function
+ ;; whicch handles state reduction
+ (set! expand
+ (lambda (state [proc-mask (list)] [to-todos? #f])
+ (if to-todos?
+ ;; repackage all the todos to have reduces representation
+ (map (lambda (td)
+ (let ([s1 (state->representative (todo-state td))]
+ [s2 (state->representative (todo->next-state td))])
+ (make-todo s1 (todo-msg td)
+ (todo-send-id td)
+ (todo-recv-id td)
+ (todo-cons-state td)
+ (todo-msg2 td)
+ s2)))
+ (stepper state proc-mask #t))
+ ;; otherwise, just map all the returned states
+ (map state->representative (stepper state proc-mask)))))
+
(set! proc-type pt)
(set! start-aut (state->state-id (vector proc-type (automaton-state1 (process-default-aut (car
(filter (lambda (x) (equal? proc-type (process-name x)))
@@ -208,8 +230,8 @@
; otherwise, check children
(begin
(let* ([new-states (filter (lambda (y) (not (hash-has-key? store y)))
- (remove-duplicates (map (lambda (x) (state->representative x store))
- (expand state))))]
+ (remove-duplicates (expand state)))]
+
; remove all states that do not have a process of proc-type in the
; initial state
@@ -301,8 +323,8 @@
(#t
(let* ([new-fr (make-hash)]
[new-states (filter (lambda (y) (not (hash-has-key? state-space y)))
- (remove-duplicates (map (lambda (x) (state->representative x state-space))
- (list-of-lists->list (map expand fr)))))]
+ (remove-duplicates
+ (list-of-lists->list (map expand fr))))]
; remove all states that do not have a process of proc-type in the
; initial state
; (because they cannot possibly simulate)
@@ -404,27 +426,21 @@
; return a list of *all* states reachable without using a transition in proc-mask
; (including the passed state)
(define explode
- (lambda (state proc-mask [to-todo #f])
+ (lambda (state proc-mask)
(let* ([collection (make-hash)]
[fringe (make-hash)])
- (if to-todo
- (begin
- ; add all start transitions
- (for-each (lambda (x) (hash-set! fringe x #t)) (expand state proc-mask #t))
- (hash-map fringe (lambda (x y) (hash-set! collection x y)))
- (explode-rec collection fringe proc-type #t))
(begin
; add start state to collection and fringe
(hash-set! fringe state (void))
(hash-set! collection state (void))
- (explode-rec collection fringe proc-mask #f))))))
+ (explode-rec collection fringe proc-mask)))))
(define explode-rec
- (lambda (collection fringe proc-mask to-todo)
- (let* ([fringe-step (remove-duplicates (list-of-lists->list (hash-map fringe
- (lambda (x y) (expand
- (state->representative (if to-todo (todo->next-state x) x) state-space)
- proc-mask to-todo)))))]
+ (lambda (collection fringe proc-mask)
+ (let* ([fringe-step (remove-duplicates
+ (list-of-lists->list
+ (hash-map fringe
+ (lambda (x y) (expand x proc-mask)))))]
[new-fringe (make-hash)])
(begin
;; add all new states in fringe-step to new-fringe and collection
@@ -434,7 +450,7 @@
(hash-set! collection x #t)
(hash-set! new-fringe x #t)))) fringe-step)
(if (= 0 (hash-count new-fringe)) (hash-map collection (lambda (x y) x))
- (explode-rec collection new-fringe proc-mask to-todo))))))
+ (explode-rec collection new-fringe proc-mask))))))
; update max-trace
;
@@ -530,8 +546,8 @@
; if start-state does not equal the initial state of the proc-type transition,
; then at least one tau transition needed to happen, first
(begin
- (if (not (equal? start-state (state->representative (todo-state td) db)))
- (connect-taus! start-state (todo-state td) db)
+ (if (not (equal? start-state (state->representative (todo-state td))))
+ (connect-taus! start-state (state->representative (todo-state td)) db)
(void))
(add-td-to-db! td db)))) (cadr entry)))))
@@ -566,7 +582,7 @@
; dummy check
(if (equal? start-state end-state) (void)
(let* ([end-db (make-hash)]
- [dmy (hash-set! end-db end-state #t)]
+ [dmy (hash-set! end-db (state->representative end-state) #t)]
[possibles (remove-duplicates (expand start-state (list proc-type-id) #t))]
; since there *is* a path to the end-state, this ormap always gives a non #f result
;
@@ -580,8 +596,8 @@
; (we need to return the first state of final-todo)
(define connect-taus-rec
(lambda (init-td final-db db)
- (let* ([start-state (state->representative (todo-state init-td) db)]
- [end-state (state->representative (todo->next-state init-td) db)]
+ (let* ([start-state (todo-state init-td)]
+ [end-state (todo->next-state init-td)]
[dmy0 (if (>= debug 4) (display-ln "ctr call:\n\tss: " start-state "\n\tes: " end-state) (void))])
(if (hash-has-key? final-db end-state)
(begin
@@ -624,41 +640,72 @@
(lambda (state mangle)
(map (lambda (x) (list-ref state x)) mangle)))
-; single-map implementation
-; (by default, use the global state-space hash for checking if a
-; representative is already present)
;
-; XXX: This means that state reduction only reduces to a single
-; representative if there is already a member of the
-; equivalence class in the state-stace.
+; maps all states to their rotation with the lowest process ids first
;
-; In other words, when the final solution path is displayed,
-; it may have system states which belong to the same
-; equivalence class, because both of them were generated
-; on the fly for searching from a particular system state.
-;
; sz: number of separate process types
;
; x: system state to check
-; sp: state-space to check against
+;
(define ring-reducer-init
(lambda (sz)
- (lambda (x [sp state-space])
- (let ([lookup (ormap (lambda (y) (hash-has-key? sp y) y #f)
- (all-rotations x sz))])
- (if lookup lookup x)))))
+ ; x: state
+ ; y: ignored
+ (lambda (x . y)
+ (car (sort (all-rotations x sz) order-by-number)))))
+; x, y are system states
+;
+; returns true if x is "less than" y
+(define (order-by-number x y)
+ ; if x and y were completely equal, just say x is first
+ (if (or (null? x) (null? y)) #t
+ (let ([xs1 (mprocess-state (car x))]
+ [ys1 (mprocess-state (car y))])
+ (cond
+ ((< xs1 ys1) #t)
+ ((> xs1 ys1) #f)
+ ;; states are equal, so compare buffers
+ (#t
+ (let* ([xbuf (mprocess-buff (car x))]
+ [ybuf (mprocess-buff (car y))]
+ [xlen (length xbuf)]
+ [ylen (length ybuf)])
+ (cond
+ ((< xlen ylen) #t)
+ ((> xlen ylen) #f)
+ ;; if message buffers are equal, give up and check the next process
+ ((equal? xbuf ybuf)
+ (order-by-number (cdr x) (cdr y)))
+ ;; otherwise, the "lower" messages go first
+ (#t
+ (which-is-first? xbuf ybuf)))))))))
+
+; like order-by-number, except for simple lists of integers
+;
+; returns true if x < y
+;
+; WARNING: this assumes that x != y and len(x) == len(y)
+(define (which-is-first? x y)
+ (let ([x1 (car x)]
+ [y1 (car y)])
+ (cond
+ ((< x1 y1) #t)
+ ((> x1 y1) #f)
+ (#t (which-is-first? (cdr x) (cdr y))))))
+
+
; return a list of all rotations of a state (including the original)
; XXX: works only for rings
(define all-rotations
(lambda (x sz)
- (let* ([times (quotient (length x) sz)]
+ (let* ([times (/ (length x) sz)]
; pieces should be a list of lists
; (of separated process types)
[pieces (chop-up x times)]
[rots (map (lambda (y)
- (list-of-lists->list
+ (list-of-lists->list
(map
(lambda (z)
(back-front z y))
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sr...@us...> - 2010-02-21 02:36:49
|
Revision: 5
http://golok.svn.sourceforge.net/golok/?rev=5&view=rev
Author: sralmai
Date: 2010-02-21 02:36:42 +0000 (Sun, 21 Feb 2010)
Log Message:
-----------
[THEORY CHANGE]: 1e models with multiple start process types are now composed
Modified Paths:
--------------
trunk/datatypes.scm
trunk/dump-1E.sh
trunk/find-k.scm
trunk/lookup-table.scm
trunk/model-builder.scm
trunk/search.scm
Modified: trunk/datatypes.scm
===================================================================
--- trunk/datatypes.scm 2010-02-20 04:40:33 UTC (rev 4)
+++ trunk/datatypes.scm 2010-02-21 02:36:42 UTC (rev 5)
@@ -47,12 +47,19 @@
item-index
;; global variables
- eps) ; keyword for no input/output msg
+ eps ; keyword for no input/output msg
+ tau ; keyword for 1e transitions between automata
+ )
;;!!! GLOBAL MAGIC VARIABLES !!!
+
+; no input transition
(define eps 'epsilon)
+; fake linking message
+(define tau 'tau)
+
;;;;;;;;;;;;;;;;;;;;;;;;; datatypes ;;;;;;;;;;;;;;;;;;;;;;;;
; state: process state
Modified: trunk/dump-1E.sh
===================================================================
--- trunk/dump-1E.sh 2010-02-20 04:40:33 UTC (rev 4)
+++ trunk/dump-1E.sh 2010-02-21 02:36:42 UTC (rev 5)
@@ -39,9 +39,7 @@
(define-values (tt mb2) (build-oneEmodel-builder prot))
-(display-ln (mb2 (car (protocol-process-names prot))))
-
(for-each (lambda (x)
(model2dot (mb2 x) (string-append output-directory "dump-1E-"
- (symbol->string x) ".dot")))
+ (symbol->string x) ".dot") #:show-buf #f))
(protocol-process-names prot))
Modified: trunk/find-k.scm
===================================================================
--- trunk/find-k.scm 2010-02-20 04:40:33 UTC (rev 4)
+++ trunk/find-k.scm 2010-02-21 02:36:42 UTC (rev 5)
@@ -191,7 +191,7 @@
(let* ([names (protocol-process-names prot)]
[name (list-ref names id)]
[mask (remove name names)])
- (let-values ([(tt oneE-builder) (build-oneEmodel-builder-new prot)])
+ (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
Modified: trunk/lookup-table.scm
===================================================================
--- trunk/lookup-table.scm 2010-02-20 04:40:33 UTC (rev 4)
+++ trunk/lookup-table.scm 2010-02-21 02:36:42 UTC (rev 5)
@@ -58,7 +58,7 @@
;; magic internal number
;;
;; (process-state / state-mod) = process-type
-(define state-mod 64)
+(define state-mod 128)
; automata: vector of automata
; refs: corresponding vector of next nodes (by index)
@@ -83,15 +83,38 @@
;;
;; topology is what is returned from instantiate-protocol
;;
-;; ((list-of automaton) topology) -> (lookup-table)
+;; ((list-of automaton)) -> (lookup-table)
;;
(define create-lookup-table
+ (lambda (automata [for-1e? #f])
+ (if for-1e? (create-1e-lookup-table automata)
+ (create-system-lookup-table automata))))
+
+;;
+;; create a lookup table (linking for 1e model)
+;;
+;; ((list-of automaton)) -> (lookup-table)
+;;
+(define create-1e-lookup-table
(lambda (automata)
(let* ([proc-map (get-processes automata)]
+ [auts-map (get-auts-map automata proc-map (get-simple-auts automata))]
+ [msgs-map (get-msgs automata)]
+ [links (create-1e-linking automata auts-map msgs-map)])
+ (make-lookup-table links auts-map (reverse-map auts-map) msgs-map (reverse-map msgs-map)
+ proc-map (reverse-map proc-map)))))
+;;
+;; create a lookup table (linking for system states)
+;;
+;; ((list-of automaton)) -> (lookup-table)
+;;
+(define create-system-lookup-table
+ (lambda (automata)
+ (let* ([proc-map (get-processes automata)]
; create a mapping from process-name and state to create a unique state ids
[states-map (get-states-map automata proc-map (get-simple-states automata))]
[msgs-map (get-msgs automata)]
- [links (create-linking automata states-map msgs-map)])
+ [links (create-sys-linking automata states-map msgs-map)])
(make-lookup-table links states-map (reverse-map states-map) msgs-map (reverse-map msgs-map) proc-map (reverse-map proc-map)))))
;; returns a hash-map with
@@ -114,6 +137,32 @@
table)))
;;
+;; create a hashmap with keys:
+;; (vector symbol? symbol? boolean?)
+;; where the first symbol is process name, second is automaton name, and third is got message?
+;; (equivalently, state 1 or 2)
+;;
+;; values are:
+;; integer?
+;; (a unique id for each automaton+state)
+;;
+;;
+(define (get-auts-map automata proc-map simple-auts-map)
+ (let ([table (make-hash)])
+ (begin
+ (for-each (lambda (x)
+ (let ([proc-id (hash-ref proc-map (automaton-proc-type x))]
+ [aut-id (hash-ref simple-auts-map (automaton-name x))])
+ (begin
+ (add-to! table (vector (automaton-proc-type x) (automaton-name x) #f)
+ (+ (* state-mod proc-id) (* 2 aut-id)))
+ (add-to! table (vector (automaton-proc-type x) (automaton-name x) #t)
+ (+ (* state-mod proc-id) (add1 (* 2 aut-id)))))))
+ automata)
+ table)))
+
+
+;;
;; returns the inverse map of passed hash-map (this assumes the map is bijective)
;;
;; (hash-map) -> (hash-map)
@@ -125,7 +174,7 @@
(hash-for-each hm (lambda (x y) (hash-set! hm2 y x)))
hm2))))
-(define create-linking
+(define create-sys-linking
(lambda (auts states-map msgs-map)
(let* ([store (make-hash)])
(begin
@@ -137,6 +186,35 @@
(cons-to-hash store (vector s1 in) (vector s2 out))))
auts)
store))))
+
+(define create-1e-linking
+ (lambda (auts auts-map msgs-map)
+ (let* ([store (make-hash)]
+ [tau-id (hash-ref msgs-map tau)])
+ (begin
+ (for-each (lambda (x)
+ (let ([s1 (hash-ref auts-map (vector (automaton-proc-type x) (automaton-name x) #f))]
+ [s2 (hash-ref auts-map (vector (automaton-proc-type x) (automaton-name x) #t))]
+ [in (hash-ref msgs-map (automaton-in-msg x))]
+ [out (hash-ref msgs-map (automaton-out-msg x))])
+ (begin
+ ;; add the labeled transition between the two states of the automaton
+ (cons-to-hash store (vector s1 in) (vector s2 out))
+ ;; all all the tau links
+ (for-each (lambda (y)
+ (let ([os1 (hash-ref auts-map (vector (automaton-proc-type y)
+ (automaton-name y) #f))]
+ [oim (hash-ref msgs-map (automaton-in-msg y))])
+ ;; if this automaton (x)'s output message equals the others (y)'s
+ ;; input message, add a tau link
+ (if (= out oim)
+ (cons-to-hash store (vector s2 tau-id) (vector os1 tau-id))
+ ; otherwise, ignore
+ (void))))
+ auts))))
+ auts)
+ store))))
+
@@ -145,7 +223,7 @@
(let ([table (make-hash)])
(begin
; add a dummy message for taus with fixed msg-id
- (add-to! table 'tau -1)
+ (add-to! table tau -2)
(for-each (lambda (x)
(begin
(add-to! table (automaton-in-msg x))
@@ -164,6 +242,22 @@
auts)
table))))
+;;
+;; Assign each automaton to an integer.
+;;
+(define get-simple-auts
+ (lambda (auts)
+ (let ([table (make-hash)])
+ (begin
+ (for-each (lambda (x)
+ (add-to! table (automaton-name x)))
+ auts)
+ table))))
+;;
+;; Add an integer label to all process types.
+;;
+;; ((list-of automaton?) -> (hash-map?)
+;;
(define get-processes
(lambda (auts)
(let ([table (make-hash)])
Modified: trunk/model-builder.scm
===================================================================
--- trunk/model-builder.scm 2010-02-20 04:40:33 UTC (rev 4)
+++ trunk/model-builder.scm 2010-02-21 02:36:42 UTC (rev 5)
@@ -17,48 +17,48 @@
;; model2dot: (model filename process-mask) -> () <dump model to graphviz "dot" output>
;;
(provide model build-sysNmodel-builder model2dot
-
- build-oneEmodel-builder-new
-
- ; (model) -> (list-of symbol?) : input messages for the first state's transitions
- ; (used in search.scm to create heuristic)
-
- ;;; alternative interface for interactive model construction
-
- ; init-stepper: (transition-model topology) -> generation-function
- ;
- ; generation-function: (state [proc-mask (list)] [to-todo #f]) -> (list-of next-states)
- init-stepper
-
- ; struct
- todo-state
-
- ; todo->label: (todo) -> (label)
- todo->label
-
- ; todo->next-state: (todo) -> (next-state)
- todo->next-state
-
- ; shared for check-specific.scm
- make-mprocess
-
+
+ build-oneEmodel-builder
+
+ ; (model) -> (list-of symbol?) : input messages for the first state's transitions
+ ; (used in search.scm to create heuristic)
+
+ ;;; alternative interface for interactive model construction
+
+ ; init-stepper: (transition-model topology) -> generation-function
+ ;
+ ; generation-function: (state [proc-mask (list)] [to-todo #f]) -> (list-of next-states)
+ init-stepper
+
+ ; struct
+ todo-state
+
+ ; todo->label: (todo) -> (label)
+ todo->label
+
+ ; todo->next-state: (todo) -> (next-state)
+ todo->next-state
+
+ ; shared for check-specific.scm
+ make-mprocess
+
; for db update
- get-id
+ get-id
+
+ ; (list-of frame?) -> (model?)
+ make-model
+
+ ; convert a hash-map of states to the first part of a struct-model
+ hash->model
+
+ ; (state trans db) -> ()
+ add-trans-to-set!
+
+ (struct-out todo)
+
+ ; shared for check-specific.scm and search.scm
+ (struct-out mprocess))
- ; (list-of frame?) -> (model?)
- make-model
-
- ; convert a hash-map of states to the first part of a struct-model
- hash->model
-
- ; (state trans db) -> ()
- add-trans-to-set!
-
- (struct-out todo)
-
- ; shared for check-specific.scm and search.scm
- (struct-out mprocess))
-
(require "datatypes.scm")
(require "lookup-table.scm")
@@ -69,7 +69,7 @@
;; !!! LOCAL MAGIC VARIABLES !!!
(define oneE-flag -317) ; used for topology and sender-id for oneEmodel generation
(define sys-prefix "a") ; prefix for node names in dot output
- ; (so state 0 is "a0" ...)
+; (so state 0 is "a0" ...)
; msg id of 'epsilon according to the trans-table
@@ -105,14 +105,14 @@
(define init-stepper
(lambda (prot topo-obj [verbose #f])
(let ([lookup-table (create-lookup-table (protocol-ba prot))])
- (let-values ([(initial-auts topo-raw) (instantiate-protocol prot topo-obj)])
- (let-values ([(topo start-state) (topo-description&initial-auts->topo-hash&start topo-raw initial-auts lookup-table)])
- (values
- (lambda (state [proc-mask (list)] [to-todos? #f])
- (let ([todos (state->todos state topo lookup-table proc-mask)])
- (if to-todos? todos
- (map todo->next-state todos)))) start-state lookup-table topo))))))
-
+ (let-values ([(initial-auts topo-raw) (instantiate-protocol prot topo-obj)])
+ (let-values ([(topo start-state) (topo-description&initial-auts->topo-hash&start topo-raw initial-auts lookup-table)])
+ (values
+ (lambda (state [proc-mask (list)] [to-todos? #f])
+ (let ([todos (state->todos state topo lookup-table proc-mask)])
+ (if to-todos? todos
+ (map todo->next-state todos)))) start-state lookup-table topo))))))
+
;;;;;;;;;;;;;;;;;;;
;;;; global function to create a model based on an initial state, full list of automata, and topo
;;;;;;;;;;;;;;;;;;;
@@ -121,36 +121,232 @@
(let ([lookup-table (create-lookup-table (protocol-ba prot))])
(lambda (topo-obj [verbose #f])
(let-values ([(initial-auts topo-raw) (instantiate-protocol prot topo-obj)])
- (let-values ([(topo start-state) (topo-description&initial-auts->topo-hash&start topo-raw initial-auts lookup-table)])
- (let* ([md (build-model start-state lookup-table topo)]
- [model (hash->model md lookup-table topo start-state)])
- (make-model model lookup-table))))))))
+ (let-values ([(topo start-state) (topo-description&initial-auts->topo-hash&start topo-raw initial-auts lookup-table)])
+ (let* ([md (build-model start-state lookup-table topo)]
+ [model (hash->model md lookup-table topo start-state)])
+ (make-model model lookup-table))))))))
;returns a model builder (which returns compact representations of 1e
; and the trans-table
-(define build-oneEmodel-builder-new
+(define build-oneEmodel-builder
(lambda (prot)
- (let ([tt (create-lookup-table (protocol-ba prot))])
- (values
- tt
- (lambda (proc-type [verbose #f] #:with-heuristics [heur? #f])
- (let* ([all-aut (protocol-ba prot)]
- [dmyyy (set! eps-id (msg->msg-id eps tt))]
- [initial-todos '()]
- [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-state1 initial-aut)) tt)]
- [initial-state (list (state->process state-id))]
- [dummy2 (if verbose (display-ln "Building oneEmodel...") (void))]
- [md (build-model initial-state tt)]
- [model (hash->model md tt oneE-flag initial-state)])
- (make-model model tt)))))))
+ (let ([tt (create-lookup-table (protocol-ba prot) #t)])
+ (values
+ tt
+ (lambda (proc-type [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))))]
+ [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)))]
+ [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
+ ; XXX
+ [stripped (strip-taus model (proc->proc-id proc-type tt) tt)]
+ [cleaned-model (reduce-model stripped)])
+ (make-model cleaned-model tt)))))))
;;
+;; strip-taus
+;;
+;; eliminates all tau transitions and transitions from another type from a given model
+;;
+;; (vector? symbol? lookup-table?) -> (vector?)
+;;
+(define (strip-taus-short raw-model proc-id lt)
+ (let* ([model (remove-tau-linking raw-model lt)])
+ model))
+
+(define (strip-taus raw-model proc-id lt)
+ (let* ([model (remove-tau-linking raw-model lt)]
+ [new-model (make-vector (vector-length model))])
+ (begin
+ ; rebuild the model (leaving out transitions)
+ (for-each (lambda (x)
+ (let ([entry (vector-ref model x)]
+ [new-entry (make-vector 2)])
+ (begin
+ ;; copy state
+ (vector-set! new-entry 0 (vector-ref entry 0))
+ ;; make blank trans list
+ (vector-set! new-entry 1 (list))
+ (vector-set! new-model x new-entry))))
+ (build-list (vector-length new-model) values))
+
+ ; for each state, for each link of type proc-id, point it to the
+ ; next state which works
+ (for-each
+ ; x is state index
+ (lambda (x)
+ ; y is a particular transition
+ (for-each
+ (lambda (y)
+ ; ends is a list of indices
+ (let ([ends (collect-endpoints (vector-ref y 3) proc-id model)])
+ (for-each
+ (lambda (z)
+ (let* ([new-tran (vector-copy y)]
+ [entry (vector-ref new-model x)]
+ [old-list (vector-ref entry 1)])
+ (begin
+ (vector-set! new-tran 3 z)
+ (vector-set! entry 1 (cons new-tran old-list))
+ (vector-set! new-model x entry))))
+ ends)))
+ (filter (lambda (a) (= proc-id (state-id->proc-id (vector-ref a 2))))
+ (vector-ref (vector-ref model x) 1))))
+ (build-list (vector-length model) values))
+
+ ;; return the model
+ new-model)))
+
+
+(define (collect-endpoints to-index proc-id model)
+ (let ([ends (make-vector 1 (list))]
+ [visit-list (make-hash)])
+ (begin
+ (collect-endpoints-rec to-index proc-id model ends visit-list)
+ (vector-ref ends 0))))
+
+
+(define (collect-endpoints-rec to-ind proc-id model ends visited-list)
+ (if (hash-has-key? visited-list to-ind)
+ ; if we've been here before, die
+ (void)
+ ;; count the out references
+ (let* ([pid-out-ids (map (lambda (x) (vector-ref x 3))
+ (filter (lambda (y) (= proc-id (state-id->proc-id (vector-ref y 2))))
+ (vector-ref (vector-ref model to-ind) 1)))]
+ [non-pid-out-ids (map (lambda (x) (vector-ref x 3))
+ (filter (lambda (y) (not (= proc-id (state-id->proc-id (vector-ref y 2)))))
+ (vector-ref (vector-ref model to-ind) 1)))])
+ (begin
+ ; mark this index
+ (hash-set! visited-list to-ind #t)
+ (cond
+ ; if there are no taus from here, just add the index that got us here and die
+ ((null? non-pid-out-ids)
+ (vector-set! ends 0 (cons to-ind (vector-ref ends 0))))
+ ; if everything is a tau transition, don't add this state, just its children
+ ((null? pid-out-ids)
+ (for-each (lambda (z) (collect-endpoints-rec z proc-id model ends visited-list)) non-pid-out-ids))
+ ; otherwise, add this state and its children
+ (#t
+ (begin
+ (vector-set! ends 0 (cons to-ind (vector-ref ends 0)))
+ (for-each (lambda (z)
+ (collect-endpoints-rec z proc-id model ends visited-list)) non-pid-out-ids))))))))
+
+;;
+;; (vector?) -> (vector?)
+;;
+(define (remove-tau-linking model lt)
+ (let ([new-model (make-vector (vector-length model))]
+ ; lookup from index in old model to index in new model
+ [old->new-map (make-hash)]
+ [tau-id (msg->msg-id tau lt)])
+ (begin
+ ;; copy needed states into new model and generate lookup table
+ (for-each
+ (lambda (x)
+ (let ([element (vector-ref model x)]
+ [size (hash-count old->new-map)])
+ ; if this is a first state (for all system processes), remember it
+ (if (all-process-states-even? (vector-ref element 0))
+ (let ([new-element (make-vector 2)])
+ (begin
+ ;; add element to lookup
+ (hash-set! old->new-map x size)
+ ;; copy state to new model
+ (vector-set! new-element 0 (vector-ref element 0))
+ ;; make blank link table
+ (vector-set! new-element 1 (list))
+ ;; copy into new model
+ (vector-set! new-model size new-element)))
+
+ ;;otherwise, ignore
+ (void))))
+ (build-list (vector-length model) values))
+
+ ;; now add links pointing in the correct places (skipping intermediates)
+ (for-each
+ (lambda (x)
+ (let ([element (vector-ref model x)])
+ ; if the state-id is even, then this is the first of the two automaton states
+ ; (and so we care about correcting where it points)
+
+ (if (not (all-process-states-even? (vector-ref element 0)))
+ ; ignore this state
+ (void)
+ ; otherwise, clean up its references
+ (for-each
+ (lambda (y)
+ (if (= tau-id (vector-ref y 0))
+ ;; skip taus here
+ (void)
+ ;; otherwise, clean up all the transitions that come from the state this
+ ;; transition leads to
+ (for-each
+ (lambda (z)
+ (if (or (not (= tau-id (vector-ref z 0)))
+ (not (hash-has-key? old->new-map (vector-ref z 3))))
+ ;; skip non-taus and transitions which go to non-start states
+ (void)
+ (let* ([new-tran (make-vector 4)]
+ [new-id (hash-ref old->new-map x)]
+ [original-entry (vector-ref new-model new-id)])
+ (begin
+ ;; copy the in and out messages and process-id
+ (vector-set! new-tran 0 (vector-ref y 0))
+ (vector-set! new-tran 1 (vector-ref y 1))
+ (vector-set! new-tran 2 (vector-ref y 2))
+ ;; copy the next-id from this transision
+ (vector-set! new-tran 3 (hash-ref old->new-map (vector-ref z 3)))
+ (vector-set! original-entry 1 (cons new-tran (vector-ref original-entry 1)))
+ (vector-set! new-model new-id original-entry)))))
+
+ (vector-ref (vector-ref model (vector-ref y 3)) 1))))
+ (vector-ref element 1)))))
+ (build-list (vector-length model) values))
+ ;; and return the new model (chopped down to size)
+ (vector-copy new-model 0 (hash-count old->new-map)))))
+
+;;
+;; create the start state for the 1e model in the case where
+;; this process starts (with first-aut) starts with epsilon
+;;
+;; (automaton? (list-of automaton?) lookup-table?) -> (list-of process?)
+;;
+(define (collect-all-eps first-aut all-aut lt)
+ (map state->process
+ (map
+ (lambda (x)
+ (state->state-id (vector (automaton-proc-type x)
+ (automaton-name x) #f) lt))
+ (cons first-aut (filter (lambda (y)
+ (and
+ (not
+ (equal?
+ (automaton-proc-type y)
+ (automaton-proc-type first-aut)))
+ (equal? (automaton-in-msg y) eps)))
+ all-aut)))))
+
+
+(define (all-process-states-even? system-state)
+ (= 0 (foldl + 0 (map (lambda (x) (modulo (mprocess-state x) 2)) system-state))))
+
+;;
;; construct a hash-map filled with all states reachable from
;; ss (the start state) with a given transition table and topology
;;
@@ -158,28 +354,28 @@
;;
(define (build-model ss tt [topo oneE-flag])
(let* ([state-space (make-hash)]
- [fringe (make-hash)]
- [dmy0 (hash-set! state-space ss #t)]
- [dmy (hash-set! fringe ss #t)])
- (build-model-rec tt fringe state-space topo)))
+ [fringe (make-hash)]
+ [dmy0 (hash-set! state-space ss #t)]
+ [dmy (hash-set! fringe ss #t)])
+ (build-model-rec tt fringe state-space topo)))
(define (build-model-rec tt fr ss topo)
(if (zero? (hash-count fr)) ss
- (let ([expanded (list-of-lists->list (hash-map fr (lambda (x y)
- (map (lambda (z)
- (todo->next-state z))
- (state->todos x topo tt)))))]
- [new-fr (make-hash)])
- (begin
+ (let ([expanded (list-of-lists->list (hash-map fr (lambda (x y)
+ (map (lambda (z)
+ (todo->next-state z))
+ (state->todos x topo tt)))))]
+ [new-fr (make-hash)])
+ (begin
(for-each
- (lambda (x)
- (if (not (hash-has-key? ss x))
- (begin (hash-set! ss x #t)
+ (lambda (x)
+ (if (not (hash-has-key? ss x))
+ (begin (hash-set! ss x #t)
(hash-set! new-fr x #t))
- (void)))
- expanded)
- (build-model-rec tt new-fr ss topo)))))
-
+ (void)))
+ expanded)
+ (build-model-rec tt new-fr ss topo)))))
+
;; dump a model to graphviz source
;;
;;
@@ -194,7 +390,7 @@
(current-output-port (open-output-file filename))
(display-ln "/* model generated by model2dot */\n\ndigraph {\n\trankdir=LR\n\n")
(for-each (lambda (x) (entry2dot x (vector-ref mdl x) lookup-table proc-mask-ids sb?))
- (build-list (vector-length mdl) values))
+ (build-list (vector-length mdl) values))
(display-ln "}")
(close-output-port (current-output-port))
(current-output-port save)))))
@@ -202,10 +398,10 @@
(define entry2dot
(lambda (index entry lt pmi sb?)
(begin
- (display-ln "\t" sys-prefix (number->string index) " [ label = \""
- (build-name (vector-ref entry 0) sb? lt)"\" ];")
- (for-each (lambda (x) (display-ln
- "\t" sys-prefix (number->string index) " -> " (trans2dot x lt pmi))) (vector-ref entry 1)))))
+ (display-ln "\t" sys-prefix (number->string index) " [ label = \""
+ (build-name (vector-ref entry 0) sb? lt)"\" ];")
+ (for-each (lambda (x) (display-ln
+ "\t" sys-prefix (number->string index) " -> " (trans2dot x lt pmi))) (vector-ref entry 1)))))
(define build-name
(lambda (state show-buf? tt)
@@ -226,145 +422,155 @@
(string-append sys-prefix
(number->string to-id) " [ label = \"" (symbol->string in) "/\\n"
(symbol->string out) "\" ]")))))
-
+
(define process2dot
(lambda (pr with-buf? tt)
(let* ([aut (state-id->state (mprocess-state pr) tt)]
[buff (mprocess-buff pr)])
(string-append (symbol->string (vector-ref aut 0)) "\\n"
- (symbol->string (vector-ref aut 1))
- (if with-buf? (string-append "\\n"
- " {" (los->string (map (lambda (x) (msg-id->msg x tt)) buff)) "}") "")))))
-
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; next state (todo) generation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
- ;; make-todos: (state link-table topology)->(list-of todo?)
- ;;
- ;;
- ;; state: list-of mprocess-struct
- ;; topo: hash-map mapping (vector recv-index recv-process-state in-msg send-index) ->
- ;; (list-of (vector new-state out-msg))
- ;; or oneE-flag
- ;;
- ;; tt: lookup-table-struct
- ;; proc-mask: list of proc-ids not to expand
- (define state->todos
- (lambda (state topo tt [proc-mask (list)])
- (let ([size (length state)])
- (flatten (map (lambda (x) (sender&msg->todos (car x) (cadr x) state tt topo proc-mask))
- ;; if building a oneE model, allow all possible inputs
- (let ([raw-input (if (equal? topo oneE-flag) (map (lambda (x) (list x oneE-flag)) (lookup-table->all-msgs tt))
- ;; always include an epsilon message with a bogus sender in available message list
- (cons (list (msg->msg-id eps tt) -1)
- (list-of-lists->list (map (lambda (x) (collect-messages state x))
- (build-list size values)))))])
- raw-input))))))
-
- ;;; state: list of processes
- ;; id: index of process in passed state from which to collect messages
- ;;; return a list of (msg proc-id) where
- (define collect-messages
- (lambda (state x)
- (let ([buff (mprocess-buff (list-ref state x))])
- (map (lambda (msg) (list msg x)) buff))))
-
- ;; collect all todos for a single sender and message
- ;; by trying every possible transition permitted by the topo
- (define sender&msg->todos
- (lambda (msg id state lt topo proc-mask)
- ; initially try to send the message to everyone
- (let* ([raw_targets (build-list (length state) values)]
- ; remove targets in proc-mask
- [targets (filter (lambda (x)
- (not (member (state-id->proc-id (mprocess-state (list-ref state x))) proc-mask))) raw_targets)])
+ (symbol->string (vector-ref aut 1))
+ (if with-buf? (string-append "\\n"
+ " {" (los->string (map (lambda (x) (msg-id->msg x tt)) buff)) "}")
+ (if (vector-ref aut 2) "\\nstate2" "\\nstate1"))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; next state (todo) generation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; make-todos: (state link-table topology)->(list-of todo?)
+;;
+;;
+;; state: list-of mprocess-struct
+;; topo: hash-map mapping (vector recv-index recv-process-state in-msg send-index) ->
+;; (list-of (vector new-state out-msg))
+;; or oneE-flag
+;;
+;; tt: lookup-table-struct
+;; proc-mask: list of proc-ids not to expand
+(define state->todos
+ (lambda (state topo tt [proc-mask (list)])
+ (let ([size (length state)])
+ (flatten (map (lambda (x) (sender&msg->todos (car x) (cadr x) state tt topo proc-mask))
+ ;; if building a oneE model, allow all possible inputs
+ (let ([raw-input (if (equal? topo oneE-flag)
+
+ ;; making a 1e model... so if not in a "start state" for all automatons,
+ (if (all-process-states-even? state)
+ ;; allow anything but taus
+ (remove (list (msg->msg-id tau tt) oneE-flag)
+ (map (lambda (x) (list x oneE-flag)) (lookup-table->all-msgs tt)))
+ ;; allow only taus
+ (list (list (msg->msg-id tau tt) oneE-flag)))
+ ;; always include an epsilon message with a bogus sender in available message list
+ (cons (list (msg->msg-id eps tt) -1)
+ (list-of-lists->list (map (lambda (x) (collect-messages state x))
+ (build-list size values)))))])
+ raw-input))))))
+
+;;; state: list of processes
+;; id: index of process in passed state from which to collect messages
+;;; return a list of (msg proc-id) where
+(define collect-messages
+ (lambda (state x)
+ (let ([buff (mprocess-buff (list-ref state x))])
+ (map (lambda (msg) (list msg x)) buff))))
+
+;; collect all todos for a single sender and message
+;; by trying every possible transition permitted by the topo
+(define sender&msg->todos
+ (lambda (msg id state lt topo proc-mask)
+ ; initially try to send the message to everyone
+ (let* ([raw_targets (build-list (length state) values)]
+ ; remove targets in proc-mask
+ [targets (filter (lambda (x)
+ (not (member (state-id->proc-id (mprocess-state (list-ref state x))) proc-mask))) raw_targets)])
(let ([result
- (list-of-lists->list
- (map
- (lambda (x)
- (sender&msg&receiver->todos msg id state x topo lt)) targets))])
- result))))
-
- ;;
- ;; sender&msg&receiver->todos: (msg id oneEmodel) -> (list-of todo?)
- ;;
- ;; given the output and id of a particular process, find other processes that can receive
- ;; the message, and return a list of todos representing this transition
- ;;
- ;; msg = message to receive
- ;; state = state creating from
- ;; recv-id = id of receiving automaton
- ;;
- ;; output: ( a list of <a-todo>)
- (define sender&msg&receiver->todos
- (lambda (msg send-id state recv-id topo lt)
- (let* ([proc (list-ref state recv-id)]
- [st (mprocess-state proc)]
- [buff (mprocess-buff proc)])
- (make-todos state msg send-id recv-id
- (if (number? topo)
- ; if oneE, give all possible transitions
- (get-trans (mprocess-state (car state)) msg lt)
- (hash-ref! topo
- (vector recv-id (mprocess-state (list-ref state recv-id)) msg send-id) (list)))))))
-
- (define make-todos
- (lambda (state msg send-id recv-id final-recv-pairs)
- (if (null? final-recv-pairs) '()
+ (list-of-lists->list
+ (map
+ (lambda (x)
+ (sender&msg&receiver->todos msg id state x topo lt)) targets))])
+ result))))
+
+;;
+;; sender&msg&receiver->todos: (msg id oneEmodel) -> (list-of todo?)
+;;
+;; given the output and id of a particular process, find other processes that can receive
+;; the message, and return a list of todos representing this transition
+;;
+;; msg = message to receive
+;; state = state creating from
+;; recv-id = id of receiving automaton
+;;
+;; output: ( a list of <a-todo>)
+(define sender&msg&receiver->todos
+ (lambda (msg send-id state recv-id topo lt)
+ (let* ([proc (list-ref state recv-id)]
+ [st (mprocess-state proc)]
+ [buff (mprocess-buff proc)])
+ (make-todos state msg send-id recv-id
+ (if (number? topo)
+ ; if oneE, give all possible transitions
+ (get-trans (mprocess-state (list-ref state recv-id)) msg lt)
+
+ (hash-ref! topo (vector recv-id (mprocess-state (list-ref state recv-id)) msg send-id)
+ (list)))))))
+
+(define make-todos
+ (lambda (state msg send-id recv-id final-recv-pairs)
+ (if (null? final-recv-pairs) '()
(let* ([tp (car final-recv-pairs)]
[new-state (vector-ref tp 0)]
[out-msg (vector-ref tp 1)])
(cons
- (make-todo state msg send-id recv-id new-state out-msg
+ (make-todo state msg send-id recv-id new-state out-msg
(make-next-state state msg send-id recv-id out-msg new-state))
- (make-todos state msg send-id recv-id (cdr final-recv-pairs)))))))
-
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; end todo generation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
- ; generate the next state from
- ; state, in-msg, send-id, recv-id, out-msg, and new process state
- (define make-next-state
- (lambda (state in-msg send-id recv-id out-msg new-pstate)
- (let* ([updated-state (clear-buffer state send-id in-msg)] ;; remove the message from the sender's out buffer
- [old-recv-buff (mprocess-buff (list-ref updated-state recv-id))]
- ;; if the message is already in the buffer, is an epsilon, or generating oneE model, don't add to the buffer
- [new-buffer (if (or (member out-msg old-recv-buff) (equal? in-msg eps) (equal? send-id oneE-flag)) old-recv-buff
-
- ;; otherwise add the message to the buffer and sort it (so states with equal buffers are "equal?")
- (sort (cons out-msg old-recv-buff) <))])
- (state-swap updated-state recv-id (make-mprocess new-pstate new-buffer)))))
-
- ;; clear-buffer (state id msg)->(state) ;; remove an element msg from process "id" in state
- (define clear-buffer
- (lambda (state id msg)
- (if (< id 0) ;; if the message had a bogus sender, don't clear anything (used for initial epsilon messages and oneE generation)
- state
- (let* ([proc (list-ref state id)]
- [new-buff (remove msg (mprocess-buff proc ))]
- [new-proc (struct-copy mprocess proc [buff new-buff])])
- (state-swap state id new-proc)))))
-
- ;; create a new state by swapping process at id out for new-proc
- (define state-swap
- (lambda (state id new-proc)
- (if (= 0 id) (cons new-proc (cdr state))
- (append (take state id) (list new-proc) (list-tail state (+ id 1))))))
-
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; functions for managing database ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
- (define state->id
- (lambda (state database)
- (let ([new-id (hash-count database)])
- (if (hash-has-key? database state)
- (values (car (hash-ref database state)) #t)
- (begin
- (hash-set! database state (list new-id '()))
- (values new-id #f))))))
-
- (define state->trans
- (lambda (state database)
- (cdar (hash-ref database state))))
-
+ (make-todos state msg send-id recv-id (cdr final-recv-pairs)))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; end todo generation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; generate the next state from
+; state, in-msg, send-id, recv-id, out-msg, and new process state
+(define make-next-state
+ (lambda (state in-msg send-id recv-id out-msg new-pstate)
+ (let* ([updated-state (clear-buffer state send-id in-msg)] ;; remove the message from the sender's out buffer
+ [old-recv-buff (mprocess-buff (list-ref updated-state recv-id))]
+ ;; if the message is already in the buffer, is an epsilon, or generating oneE model, don't add to the buffer
+ [new-buffer (if (or (member out-msg old-recv-buff) (equal? in-msg eps) (equal? send-id oneE-flag)) old-recv-buff
+
+ ;; otherwise add the message to the buffer and sort it (so states with equal buffers are "equal?")
+ (sort (cons out-msg old-recv-buff) <))])
+ (state-swap updated-state recv-id (make-mprocess new-pstate new-buffer)))))
+
+;; clear-buffer (state id msg)->(state) ;; remove an element msg from process "id" in state
+(define clear-buffer
+ (lambda (state id msg)
+ (if (< id 0) ;; if the message had a bogus sender, don't clear anything (used for initial epsilon messages and oneE generation)
+ state
+ (let* ([proc (list-ref state id)]
+ [new-buff (remove msg (mprocess-buff proc ))]
+ [new-proc (struct-copy mprocess proc [buff new-buff])])
+ (state-swap state id new-proc)))))
+
+;; create a new state by swapping process at id out for new-proc
+(define state-swap
+ (lambda (state id new-proc)
+ (if (= 0 id) (cons new-proc (cdr state))
+ (append (take state id) (list new-proc) (list-tail state (+ id 1))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; functions for managing database ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define state->id
+ (lambda (state database)
+ (let ([new-id (hash-count database)])
+ (if (hash-has-key? database state)
+ (values (car (hash-ref database state)) #t)
+ (begin
+ (hash-set! database state (list new-id '()))
+ (values new-id #f))))))
+
+(define state->trans
+ (lambda (state database)
+ (cdar (hash-ref database state))))
+
;;;;;;;;;;;;;;;;
; general utilities
@@ -374,7 +580,7 @@
[id (car entry)]
[old-list (cadr entry)])
(if (member trans old-list) (void)
- (hash-set! db state (list id (cons trans old-list)))))))
+ (hash-set! db state (list id (cons trans old-list)))))))
;;
@@ -398,31 +604,31 @@
(lambda (sp tt topo [ss #f] [state->representative (lambda (x . y) x)])
(let ([db (make-hash)])
(begin
- ; ensure the start state gets id 0
+ ; ensure the start state gets id 0
(if ss (get-id ss db) (void))
- ; dump all states into db
+ ; dump all states into db
(hash-for-each sp (lambda (x y) (get-id x db)))
- ; dump all transitions into db
+ ; dump all transitions into db
(hash-for-each sp (lambda (x y)
- (let ([todos (state->todos x topo tt)])
- (for-each
- (lambda (z)
- (let* ([ss-id (get-id (state->representative (todo-state z) sp) db)]
- [to-id (get-id (state->representative (todo->next-state z) sp) db)])
- (add-trans-to-set! (todo-state z) (todo->label to-id z) db)))
- (filter (lambda (g) (hash-has-key? db (state->representative (todo->next-state g) sp))) todos)))))
- (let ([vect (make-vector (hash-count db))])
- (begin
- (hash-for-each db (lambda (x y)
- (let ([id (car y)]
- [list-of-trans (cadr y)])
- (vector-set! vect id (vector x list-of-trans)))))
- vect))))))
+ (let ([todos (state->todos x topo tt)])
+ (for-each
+ (lambda (z)
+ (let* ([ss-id (get-id (state->representative (todo-state z) sp) db)]
+ [to-id (get-id (state->representative (todo->next-state z) sp) db)])
+ (add-trans-to-set! (todo-state z) (todo->label to-id z) db)))
+ (filter (lambda (g) (hash-has-key? db (state->representative (todo->next-state g) sp))) todos)))))
+ (let ([vect (make-vector (hash-count db))])
+ (begin
+ (hash-for-each db (lambda (x y)
+ (let ([id (car y)]
+ [list-of-trans (cadr y)])
+ (vector-set! vect id (vector x list-of-trans)))))
+ vect))))))
(define (todo->label to-id td)
(let ([in (todo-msg td)]
[out (todo-msg2 td)]
- ; saved for filtering (on process type)
+ ; saved for filtering (on process type)
[new-state (todo-cons-state td)])
(vector in out new-state to-id)))
@@ -434,3 +640,199 @@
(begin
(hash-set! db state (list new-id (list)))
new-id)))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; reduce model ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; remove duplicate transitions from given model and returns new model
+(define reduce-model
+ (lambda (md)
+ (let* ([new-md (vector-copy md)]
+ [dummy (for-each (lambda (x) (strip-dups x new-md)) (build-list (vector-length new-md) values))]
+ [original-ends (mark-singletons md)]
+ [dummy1 (remove-dead-nodes new-md original-ends)])
+ new-md)))
+
+;;
+;; helper for rec-strip
+;;
+;; returns true iff the in and out messages of the two transitions is equal
+;;
+(define (labels-eq? t1 t2)
+ (and (= (vector-ref t1 0) (vector-ref t2 0)) (= (vector-ref t1 1) (vector-ref t2 1))))
+
+;; top level caller for "trace"... calls trace on all duplicates
+(define strip-dups
+ (lambda (index md)
+ (rec-strip-dups 0 index md)))
+
+(define rec-strip-dups
+ (lambda (trans-index index md)
+ (let ([full-list (vector-ref (vector-ref md index) 1)])
+ (if
+ (>= trans-index (length full-list)) (void) ; done
+ (let* ([trans-list (list-tail full-list (+ 1 trans-index))]
+ [trans-to-match (list-ref (vector-ref (vector-ref md index) 1) trans-index)]
+ [matching (filter (lambda (x) (labels-eq? trans-to-match x)) trans-list)])
+ (if (not (null? matching))
+ (if (trace index trans-to-match (car matching) md)
+ (rec-strip-dups trans-index index md) ; we made a change, so run against the same trans again
+ (rec-strip-dups (+ 1 trans-index) index md)) ; otherwise, move on
+ (rec-strip-dups (+ 1 trans-index) index md))))))) ; ditto here
+
+;;
+;; Returns a vector of #t/#f values tagging all the non-looped nodes in the model.
+;; This is necessary to prevent them from being cleared in the "remove-dead-nodes"
+;; function.
+;;
+;; (Checking for duplicate paths works by deleting the final parallel link and
+;; then cleaning up the dead ends back to the branch point. But we need to
+;; differentiate between non-loops in the original model and dead ends introduced
+;; by the duplicate path identification algorithm.)
+;;
+;; (vector?) -> (vector?)
+(define mark-singletons
+ (lambda (mdl)
+ (let ([mark-list (make-vector (vector-length mdl) #f)]
+ [visited (make-vector (vector-length mdl) #f)])
+ (begin
+ (mark-rec 0 mdl mark-list visited)
+ mark-list))))
+
+(define mark-rec
+ (lambda (index mdl mark-list visited)
+ ; we've been here before, return whether or not we are part of a deadend path
+ (if (vector-ref visited index) (vector-ref mark-list index)
+ (begin
+ ; mark this node as visited
+ (vector-set! visited index #t)
+ ; if this is a deadend, mark it and return true
+ (cond
+ ((zero? (length (vector-ref (vector-ref mdl index) 1)))
+ (begin
+ (vector-set! mark-list index #t) #t))
+ ; otherwise, if all children are dead ends, do the same
+ ((andmap (lambda (x) (mark-rec x mdl mark-list visited))
+ (map (lambda (z) (vector-ref z 3)) (vector-ref (vector-ref mdl index) 1)))
+ (begin
+ (vector-set! mark-list index #t) #t))
+ (#t
+ ; otherwise, we are not part of a dead end
+ #f))))))
+
+;;
+;; strips non-loop transitions from md (except for nodes in blacklist)
+;;
+(define remove-dead-nodes
+ (lambda (md blacklist)
+ (let ([out-count (build-vector (vector-length md) (lambda (x) (list (length (vector-ref (vector-ref md x) 1)) x)))]
+ [rev-g (reverse-graph md)])
+ (remove-dead-rec out-count md rev-g blacklist))))
+
+(define remove-dead-rec
+ (lambda (out-count md rev-g blacklist)
+ (let ([first (assoc 0 (vector->list out-count))])
+ (if first
+ (let ([index (cadr first)])
+ (begin
+ ; if this is on the blacklist, do not remove the link
+ (if (vector-ref blacklist index)
+ (void)
+ ; otherwise, this was part of a duplicate path, so remove it
+ (remove-node index md rev-g out-count))
+ (vector-set! out-count index (list -1 index)) ; mark this end node as checked
+ (remove-dead-rec out-count md rev-g blacklist)))
+
+ (void))))) ; otherwise, finished
+
+;; remove all transitions to <index> in <md>
+(define remove-node
+ (lambda (index md rev-g count-g)
+ (let ([nodes-with-trans-to (map (lambda (x) (vector-ref x 3)) (vector-ref (vector-ref rev-g index) 1))])
+ (for-each (lambda (x) (for-each
+ (lambda (y)
+ (begin
+ (del-trans md x y)
+ ; update reference count
+ (vector-set! count-g x (list (- (car (vector-ref count-g x)) 1) x))))
+ (filter
+ (lambda (z) (eq? (vector-ref z 3) index)) (vector-ref (vector-ref md x) 1))))
+ nodes-with-trans-to))))
+
+
+(define reverse-graph
+ (lambda (md)
+ (let* ([size (vector-length md)]
+ [new-md (build-vector size (lambda (x) (make-vector 2)))])
+ (begin
+ ;; set up all elements of the new model with state information and blank transitions
+ (for-each (lambda (x)
+ (let ([element (make-vector 2)])
+ (begin
+ ; copy state
+ (vector-set! element 0 (vector-ref (vector-ref md x) 0))
+ ; create empty list of transitions
+ (vector-set! element 1 (list))
+ (vector-set! new-md x element))))
+ (build-list size values))
+
+ ;; add all reversed transitions
+ (for-each (lambda (x) (reverse-element x (vector-ref (vector-ref md x) 1) new-md)) (build-list size values))
+
+ ;; return the created reverse map
+ new-md))))
+
+(define trace
+ ; id: index of state with eq? labeled transitions
+ ; t1, t2: eq? labeled transitions
+ ; md: model referred to
+ (lambda (id t1 t2 md)
+ (let ([res (trace-rec (list (list id t1)) (list (list id t2)) md)])
+ (if res
+ (begin
+ (for-each (lambda (x) (del-trans md (car x) (cadr x))) res)
+ #t)
+ #f))))
+
+; search for a continuation of equivalent transitions
+(define trace-rec
+ (lambda (l1 l2 md)
+ (let ([id1 (vector-ref (cadar l1) 3)]
+ [id2 (vector-ref (cadar l2) 3)])
+ (if (= id1 id2) ; hit simulation
+ l2
+ (let ([trans1 (vector-ref (vector-ref md id1) 1)]
+ [trans2 (vector-ref (vector-ref md id2) 1)])
+ (if
+ (and (= (length trans1) 1) (= (length trans2) 1) (labels-eq? (car trans1) (car trans2)))
+ (trace-rec (cons (list id1 (car trans1)) l1) (cons (list id2 (car trans2)) l2) md)
+ #f))))))
+
+(define reverse-element
+ (lambda (new-end lot mdl)
+ (for-each (lambda (x)
+ (add-trans mdl (vector-ref x 3) new-end (vector-copy x))) lot)))
+
+;;
+;; lbl : a vector of length 4 < in-msg-id, out-msg-id, new-state-id, to-id (replaced with end) >
+;; end : new to-id (index in mdl that this transition leads to)
+;;
+(define add-trans
+ (lambda (mdl start end lbl)
+ (let* ([cur (vector-ref mdl start)]
+ [cur-trans (vector-ref cur 1)])
+ (begin
+ ; replace endpoint with new end index
+ (vector-set! lbl 3 end)
+ ; add this transition to the transition list for the new start element
+ (vector-set! cur 1 (cons lbl cur-trans))
+ (vector-set! mdl start cur)))))
+
+(define del-trans
+ (lambda (mdl index tr)
+ (let* ([cur (vector-ref mdl index)]
+ [cur-trans (vector-ref cur 1)]
+ [new-trans (remove tr cur-trans)]
+ [dmy (vector-set! cur 1 new-trans)])
+ (vector-set! mdl index cur))))
Modified: trunk/search.scm
===================================================================
--- trunk/search.scm 2010-02-20 04:40:33 UTC (rev 4)
+++ trunk/search.scm 2010-02-21 02:36:42 UTC (rev 5)
@@ -163,7 +163,7 @@
(set! proc-type-id (proc->proc-id proc-type lt))
(set! other-mask-ids (map (lambda (x) (proc->proc-id x lt)) other-mask))
- (let-values ([(fresh-tt builder) (build-oneEmodel-builder-new prot)])
+ (let-values ([(fresh-tt builder) (build-oneEmodel-builder prot)])
(set! oneE (model-mdl (builder proc-type))))
; debugging messages
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
