Plan 9 from Bell Labs 2007-08-08

dist/replica/_plan9.db

@@ -5517,7 +5517,7 @@ rc/bin/kmem - 775 sys sys 1141940177 468
 rc/bin/label - 775 sys sys 1173737765 189
 rc/bin/lc - 775 sys sys 945617207 24
 rc/bin/leak - 775 sys sys 1172760642 1921
-rc/bin/lookman - 775 sys sys 1017679344 686
+rc/bin/lookman - 775 sys sys 1186528516 687
 rc/bin/lp - 775 sys sys 1162105982 5201
 rc/bin/mail - 775 sys sys 1045504003 138
 rc/bin/man - 775 sys sys 1174803269 2639
@@ -7445,7 +7445,7 @@ sys/man/1/size - 664 sys sys 944959674 393
 sys/man/1/sleep - 664 sys sys 1167774352 420
 sys/man/1/sort - 664 sys sys 1113743328 4719
 sys/man/1/spell - 664 sys sys 1113743329 1876
-sys/man/1/spin - 664 sys sys 1142177238 7246
+sys/man/1/spin - 664 sys sys 1186525444 6685
 sys/man/1/split - 664 sys sys 1038183072 1171
 sys/man/1/src - 664 sys sys 954266293 1138
 sys/man/1/ssh - 664 sys sys 1048643947 6622
@@ -13419,45 +13419,45 @@ sys/src/cmd/spell/spell.rc - 775 sys sys 964457135 312
 sys/src/cmd/spell/sprog.c - 664 sys sys 1143759342 23038
 sys/src/cmd/spell/stop - 664 sys sys 944961232 18702
 sys/src/cmd/spin - 20000000775 sys sys 1125514861 0
-sys/src/cmd/spin/README - 664 sys sys 1125514858 311
-sys/src/cmd/spin/dstep.c - 664 sys sys 1125514858 9958
-sys/src/cmd/spin/flow.c - 664 sys sys 1125514858 17345
-sys/src/cmd/spin/guided.c - 664 sys sys 1125514858 6948
-sys/src/cmd/spin/main.c - 664 sys sys 1125514858 21713
-sys/src/cmd/spin/mesg.c - 664 sys sys 1125514858 13722
+sys/src/cmd/spin/README - 664 sys sys 1186525913 311
+sys/src/cmd/spin/dstep.c - 664 sys sys 1186525913 10009
+sys/src/cmd/spin/flow.c - 664 sys sys 1186525914 17303
+sys/src/cmd/spin/guided.c - 664 sys sys 1186525914 7045
+sys/src/cmd/spin/main.c - 664 sys sys 1186525914 21670
+sys/src/cmd/spin/mesg.c - 664 sys sys 1186525914 14109
 sys/src/cmd/spin/mkfile - 664 sys sys 1125514859 696
-sys/src/cmd/spin/pangen1.c - 664 sys sys 1125514859 29801
-sys/src/cmd/spin/pangen1.h - 664 sys sys 1125514859 134192
-sys/src/cmd/spin/pangen2.c - 664 sys sys 1125514859 74348
-sys/src/cmd/spin/pangen2.h - 664 sys sys 1125514860 23109
-sys/src/cmd/spin/pangen3.c - 664 sys sys 1125514860 8941
-sys/src/cmd/spin/pangen3.h - 664 sys sys 1125514860 22484
-sys/src/cmd/spin/pangen4.c - 664 sys sys 1125514860 8180
-sys/src/cmd/spin/pangen4.h - 664 sys sys 1125514860 19033
-sys/src/cmd/spin/pangen5.c - 664 sys sys 1125514860 16851
+sys/src/cmd/spin/pangen1.c - 664 sys sys 1186525914 31423
+sys/src/cmd/spin/pangen1.h - 664 sys sys 1186525915 137482
+sys/src/cmd/spin/pangen2.c - 664 sys sys 1186525916 75808
+sys/src/cmd/spin/pangen2.h - 664 sys sys 1186525916 23811
+sys/src/cmd/spin/pangen3.c - 664 sys sys 1186525916 8914
+sys/src/cmd/spin/pangen3.h - 664 sys sys 1186525916 22760
+sys/src/cmd/spin/pangen4.c - 664 sys sys 1186525916 8138
+sys/src/cmd/spin/pangen4.h - 664 sys sys 1186525917 19034
+sys/src/cmd/spin/pangen5.c - 664 sys sys 1186525917 16809
 sys/src/cmd/spin/pangen5.h - 664 sys sys 1125514861 11145
-sys/src/cmd/spin/pangen6.c - 664 sys sys 1125514861 48633
-sys/src/cmd/spin/pc_zpp.c - 664 sys sys 1125514861 8737
+sys/src/cmd/spin/pangen6.c - 664 sys sys 1186525917 48587
+sys/src/cmd/spin/pc_zpp.c - 664 sys sys 1186525918 8745
 sys/src/cmd/spin/ps_msc.c - 664 sys sys 1125514861 11872
-sys/src/cmd/spin/reprosrc.c - 664 sys sys 1125514861 2978
-sys/src/cmd/spin/run.c - 664 sys sys 1125514862 14405
-sys/src/cmd/spin/sched.c - 664 sys sys 1125514862 21096
-sys/src/cmd/spin/spin.h - 664 sys sys 1125514862 12286
-sys/src/cmd/spin/spin.y - 664 sys sys 1125514862 18876
-sys/src/cmd/spin/spinlex.c - 664 sys sys 1125514862 30767
-sys/src/cmd/spin/structs.c - 664 sys sys 1125514863 14150
-sys/src/cmd/spin/sym.c - 664 sys sys 1125514863 11863
+sys/src/cmd/spin/reprosrc.c - 664 sys sys 1186525918 2936
+sys/src/cmd/spin/run.c - 664 sys sys 1186525918 14364
+sys/src/cmd/spin/sched.c - 664 sys sys 1186525918 21862
+sys/src/cmd/spin/spin.h - 664 sys sys 1186525918 12331
+sys/src/cmd/spin/spin.y - 664 sys sys 1186525919 19060
+sys/src/cmd/spin/spinlex.c - 664 sys sys 1186525919 31555
+sys/src/cmd/spin/structs.c - 664 sys sys 1186525920 14108
+sys/src/cmd/spin/sym.c - 664 sys sys 1186525920 11879
 sys/src/cmd/spin/tl.h - 664 sys sys 1125514863 3332
 sys/src/cmd/spin/tl_buchi.c - 664 sys sys 1125514863 13080
 sys/src/cmd/spin/tl_cache.c - 664 sys sys 1125514863 5831
-sys/src/cmd/spin/tl_lex.c - 664 sys sys 1125514863 3243
-sys/src/cmd/spin/tl_main.c - 664 sys sys 1125514863 4412
+sys/src/cmd/spin/tl_lex.c - 664 sys sys 1186525920 3244
+sys/src/cmd/spin/tl_main.c - 664 sys sys 1186525920 4679
 sys/src/cmd/spin/tl_mem.c - 664 sys sys 1125514864 2670
-sys/src/cmd/spin/tl_parse.c - 664 sys sys 1125514864 8257
+sys/src/cmd/spin/tl_parse.c - 664 sys sys 1186525921 8348
 sys/src/cmd/spin/tl_rewrt.c - 664 sys sys 1125514864 5962
 sys/src/cmd/spin/tl_trans.c - 664 sys sys 1125514864 16758
-sys/src/cmd/spin/vars.c - 664 sys sys 1125514864 8393
-sys/src/cmd/spin/version.h - 664 sys sys 1125514864 53
+sys/src/cmd/spin/vars.c - 664 sys sys 1186525921 8374
+sys/src/cmd/spin/version.h - 664 sys sys 1186525921 53
 sys/src/cmd/split.c - 664 sys sys 1116770353 3225
 sys/src/cmd/srv.c - 664 sys sys 1144685254 4003
 sys/src/cmd/srvfs.c - 664 sys sys 1161442157 1726

dist/replica/plan9.db

@@ -5517,7 +5517,7 @@ rc/bin/kmem - 775 sys sys 1141940177 468
 rc/bin/label - 775 sys sys 1173737765 189
 rc/bin/lc - 775 sys sys 945617207 24
 rc/bin/leak - 775 sys sys 1172760642 1921
-rc/bin/lookman - 775 sys sys 1017679344 686
+rc/bin/lookman - 775 sys sys 1186528516 687
 rc/bin/lp - 775 sys sys 1162105982 5201
 rc/bin/mail - 775 sys sys 1045504003 138
 rc/bin/man - 775 sys sys 1174803269 2639
@@ -7445,7 +7445,7 @@ sys/man/1/size - 664 sys sys 944959674 393
 sys/man/1/sleep - 664 sys sys 1167774352 420
 sys/man/1/sort - 664 sys sys 1113743328 4719
 sys/man/1/spell - 664 sys sys 1113743329 1876
-sys/man/1/spin - 664 sys sys 1142177238 7246
+sys/man/1/spin - 664 sys sys 1186525444 6685
 sys/man/1/split - 664 sys sys 1038183072 1171
 sys/man/1/src - 664 sys sys 954266293 1138
 sys/man/1/ssh - 664 sys sys 1048643947 6622
@@ -13419,45 +13419,45 @@ sys/src/cmd/spell/spell.rc - 775 sys sys 964457135 312
 sys/src/cmd/spell/sprog.c - 664 sys sys 1143759342 23038
 sys/src/cmd/spell/stop - 664 sys sys 944961232 18702
 sys/src/cmd/spin - 20000000775 sys sys 1125514861 0
-sys/src/cmd/spin/README - 664 sys sys 1125514858 311
-sys/src/cmd/spin/dstep.c - 664 sys sys 1125514858 9958
-sys/src/cmd/spin/flow.c - 664 sys sys 1125514858 17345
-sys/src/cmd/spin/guided.c - 664 sys sys 1125514858 6948
-sys/src/cmd/spin/main.c - 664 sys sys 1125514858 21713
-sys/src/cmd/spin/mesg.c - 664 sys sys 1125514858 13722
+sys/src/cmd/spin/README - 664 sys sys 1186525913 311
+sys/src/cmd/spin/dstep.c - 664 sys sys 1186525913 10009
+sys/src/cmd/spin/flow.c - 664 sys sys 1186525914 17303
+sys/src/cmd/spin/guided.c - 664 sys sys 1186525914 7045
+sys/src/cmd/spin/main.c - 664 sys sys 1186525914 21670
+sys/src/cmd/spin/mesg.c - 664 sys sys 1186525914 14109
 sys/src/cmd/spin/mkfile - 664 sys sys 1125514859 696
-sys/src/cmd/spin/pangen1.c - 664 sys sys 1125514859 29801
-sys/src/cmd/spin/pangen1.h - 664 sys sys 1125514859 134192
-sys/src/cmd/spin/pangen2.c - 664 sys sys 1125514859 74348
-sys/src/cmd/spin/pangen2.h - 664 sys sys 1125514860 23109
-sys/src/cmd/spin/pangen3.c - 664 sys sys 1125514860 8941
-sys/src/cmd/spin/pangen3.h - 664 sys sys 1125514860 22484
-sys/src/cmd/spin/pangen4.c - 664 sys sys 1125514860 8180
-sys/src/cmd/spin/pangen4.h - 664 sys sys 1125514860 19033
-sys/src/cmd/spin/pangen5.c - 664 sys sys 1125514860 16851
+sys/src/cmd/spin/pangen1.c - 664 sys sys 1186525914 31423
+sys/src/cmd/spin/pangen1.h - 664 sys sys 1186525915 137482
+sys/src/cmd/spin/pangen2.c - 664 sys sys 1186525916 75808
+sys/src/cmd/spin/pangen2.h - 664 sys sys 1186525916 23811
+sys/src/cmd/spin/pangen3.c - 664 sys sys 1186525916 8914
+sys/src/cmd/spin/pangen3.h - 664 sys sys 1186525916 22760
+sys/src/cmd/spin/pangen4.c - 664 sys sys 1186525916 8138
+sys/src/cmd/spin/pangen4.h - 664 sys sys 1186525917 19034
+sys/src/cmd/spin/pangen5.c - 664 sys sys 1186525917 16809
 sys/src/cmd/spin/pangen5.h - 664 sys sys 1125514861 11145
-sys/src/cmd/spin/pangen6.c - 664 sys sys 1125514861 48633
-sys/src/cmd/spin/pc_zpp.c - 664 sys sys 1125514861 8737
+sys/src/cmd/spin/pangen6.c - 664 sys sys 1186525917 48587
+sys/src/cmd/spin/pc_zpp.c - 664 sys sys 1186525918 8745
 sys/src/cmd/spin/ps_msc.c - 664 sys sys 1125514861 11872
-sys/src/cmd/spin/reprosrc.c - 664 sys sys 1125514861 2978
-sys/src/cmd/spin/run.c - 664 sys sys 1125514862 14405
-sys/src/cmd/spin/sched.c - 664 sys sys 1125514862 21096
-sys/src/cmd/spin/spin.h - 664 sys sys 1125514862 12286
-sys/src/cmd/spin/spin.y - 664 sys sys 1125514862 18876
-sys/src/cmd/spin/spinlex.c - 664 sys sys 1125514862 30767
-sys/src/cmd/spin/structs.c - 664 sys sys 1125514863 14150
-sys/src/cmd/spin/sym.c - 664 sys sys 1125514863 11863
+sys/src/cmd/spin/reprosrc.c - 664 sys sys 1186525918 2936
+sys/src/cmd/spin/run.c - 664 sys sys 1186525918 14364
+sys/src/cmd/spin/sched.c - 664 sys sys 1186525918 21862
+sys/src/cmd/spin/spin.h - 664 sys sys 1186525918 12331
+sys/src/cmd/spin/spin.y - 664 sys sys 1186525919 19060
+sys/src/cmd/spin/spinlex.c - 664 sys sys 1186525919 31555
+sys/src/cmd/spin/structs.c - 664 sys sys 1186525920 14108
+sys/src/cmd/spin/sym.c - 664 sys sys 1186525920 11879
 sys/src/cmd/spin/tl.h - 664 sys sys 1125514863 3332
 sys/src/cmd/spin/tl_buchi.c - 664 sys sys 1125514863 13080
 sys/src/cmd/spin/tl_cache.c - 664 sys sys 1125514863 5831
-sys/src/cmd/spin/tl_lex.c - 664 sys sys 1125514863 3243
-sys/src/cmd/spin/tl_main.c - 664 sys sys 1125514863 4412
+sys/src/cmd/spin/tl_lex.c - 664 sys sys 1186525920 3244
+sys/src/cmd/spin/tl_main.c - 664 sys sys 1186525920 4679
 sys/src/cmd/spin/tl_mem.c - 664 sys sys 1125514864 2670
-sys/src/cmd/spin/tl_parse.c - 664 sys sys 1125514864 8257
+sys/src/cmd/spin/tl_parse.c - 664 sys sys 1186525921 8348
 sys/src/cmd/spin/tl_rewrt.c - 664 sys sys 1125514864 5962
 sys/src/cmd/spin/tl_trans.c - 664 sys sys 1125514864 16758
-sys/src/cmd/spin/vars.c - 664 sys sys 1125514864 8393
-sys/src/cmd/spin/version.h - 664 sys sys 1125514864 53
+sys/src/cmd/spin/vars.c - 664 sys sys 1186525921 8374
+sys/src/cmd/spin/version.h - 664 sys sys 1186525921 53
 sys/src/cmd/split.c - 664 sys sys 1116770353 3225
 sys/src/cmd/srv.c - 664 sys sys 1144685254 4003
 sys/src/cmd/srvfs.c - 664 sys sys 1161442157 1726

dist/replica/plan9.log

@@ -49866,3 +49866,35 @@
 1186371003 0 c 386/bin/htmlfmt - 775 sys sys 1186370974 163412
 1186371003 1 c 386/lib/libhtml.a - 664 sys sys 1186370975 229202
 1186407005 0 c sys/src/9/ip/tcp.c - 664 sys sys 1186406232 65963
+1186525804 0 c sys/man/1/spin - 664 sys sys 1186525444 6685
+1186527604 0 c sys/src/cmd/spin/README - 664 sys sys 1186525913 311
+1186527604 1 c sys/src/cmd/spin/dstep.c - 664 sys sys 1186525913 10009
+1186527604 2 c sys/src/cmd/spin/flow.c - 664 sys sys 1186525914 17303
+1186527604 3 c sys/src/cmd/spin/guided.c - 664 sys sys 1186525914 7045
+1186527604 4 c sys/src/cmd/spin/main.c - 664 sys sys 1186525914 21670
+1186527604 5 c sys/src/cmd/spin/mesg.c - 664 sys sys 1186525914 14109
+1186527604 6 c sys/src/cmd/spin/pangen1.c - 664 sys sys 1186525914 31423
+1186527604 7 c sys/src/cmd/spin/pangen1.h - 664 sys sys 1186525915 137482
+1186527604 8 c sys/src/cmd/spin/pangen2.c - 664 sys sys 1186525916 75808
+1186527604 9 c sys/src/cmd/spin/pangen2.h - 664 sys sys 1186525916 23811
+1186527604 10 c sys/src/cmd/spin/pangen3.c - 664 sys sys 1186525916 8914
+1186527604 11 c sys/src/cmd/spin/pangen3.h - 664 sys sys 1186525916 22760
+1186527604 12 c sys/src/cmd/spin/pangen4.c - 664 sys sys 1186525916 8138
+1186527604 13 c sys/src/cmd/spin/pangen4.h - 664 sys sys 1186525917 19034
+1186527604 14 c sys/src/cmd/spin/pangen5.c - 664 sys sys 1186525917 16809
+1186527604 15 c sys/src/cmd/spin/pangen6.c - 664 sys sys 1186525917 48587
+1186527604 16 c sys/src/cmd/spin/pc_zpp.c - 664 sys sys 1186525918 8745
+1186527604 17 c sys/src/cmd/spin/reprosrc.c - 664 sys sys 1186525918 2936
+1186527604 18 c sys/src/cmd/spin/run.c - 664 sys sys 1186525918 14364
+1186527604 19 c sys/src/cmd/spin/sched.c - 664 sys sys 1186525918 21862
+1186527604 20 c sys/src/cmd/spin/spin.h - 664 sys sys 1186525918 12331
+1186527604 21 c sys/src/cmd/spin/spin.y - 664 sys sys 1186525919 19060
+1186527604 22 c sys/src/cmd/spin/spinlex.c - 664 sys sys 1186525919 31555
+1186527604 23 c sys/src/cmd/spin/structs.c - 664 sys sys 1186525920 14108
+1186527604 24 c sys/src/cmd/spin/sym.c - 664 sys sys 1186525920 11879
+1186527604 25 c sys/src/cmd/spin/tl_lex.c - 664 sys sys 1186525920 3244
+1186527604 26 c sys/src/cmd/spin/tl_main.c - 664 sys sys 1186525920 4679
+1186527604 27 c sys/src/cmd/spin/tl_parse.c - 664 sys sys 1186525921 8348
+1186527604 28 c sys/src/cmd/spin/vars.c - 664 sys sys 1186525921 8374
+1186527604 29 c sys/src/cmd/spin/version.h - 664 sys sys 1186525921 53
+1186529404 0 c rc/bin/lookman - 775 sys sys 1186528516 687

rc/bin/lookman

@@ -8,7 +8,7 @@ fn sigexit sigint sighup sigterm{
 	rm -f $t1 $t2
 	exit 1
 }
-*=`{echo $*|tr A-Z a-z|tr -dc 'a-z0-9_ \012'}	# fold case, delete funny chars
+*=`{echo $*|tr A-Z a-z|tr -dc 'a-z0-9_. \012'}	# fold case, delete funny chars
 if(~ $#* 0){
 	echo Usage: lookman key ... >/fd/2
 	exit 1

sys/man/1/spin

@@ -1,6 +1,6 @@
 .TH SPIN 1
 .SH NAME
-spin \- verification tool for models of concurrent systems
+spin - verification tool for models of concurrent systems
 .SH SYNOPSIS
 .B spin
 .B -a
@@ -93,7 +93,8 @@ is a tool for analyzing the logical consistency of
 asynchronous systems, specifically distributed software
 amd communication protocols.
 A verification model of the system is first specified
-in a guarded command language called Promela.
+in a guarded command language called
+.IR Promela .
 This specification language, described in the reference,
 allows for the modeling of dynamic creation of
 asynchronous processes,
@@ -103,18 +104,15 @@ It also allows for a concise specification of logical
 correctness requirements, including, but not restricted
 to requirements expressed in linear temporal logic.
 .PP
-Given a Promela model
-stored in
-.I file ,
+Given a Promela model stored in
+.IR file ,
 .I spin
 can perform interactive, guided, or random simulations
 of the system's execution.
 It can also generate a C program that performs an exhaustive
 or approximate verification of the correctness requirements
 for the system.
-.PP
-The basic command options are:
-.\"----------------------a----------------
+.
 .TP
 .B -a
 Generate a verifier (model checker) for the specification.
@@ -127,20 +125,19 @@ The online
 .I spin
 manuals (see below) contain
 the details on compilation and use of the verifiers.
-.\"--------------------------c------------
+.
 .TP
 .B -c
 Produce an ASCII approximation of a message sequence
-chart for a random or guided (when combined with 
+chart for a random or guided (when combined with
 .BR -t )
-simulation run. 
-See also option
+simulation run. See also option
 .BR -M .
-.\"--------------------------d------------
+.
 .TP
-.BI -d
+.B -d
 Produce symbol table information for the model specified in
-.I file .
+.IR file .
 For each Promela object this information includes the type, name and
 number of elements (if declared as an array), the initial
 value (if a data object) or size (if a message channel), the
@@ -149,24 +146,28 @@ a variable or as a parameter.  For message channels, the data types
 of the message fields are listed.
 For structure variables, the third field defines the
 name of the structure declaration that contains the variable.
-.\"--------------------------f------------
+.
 .TP
-.B "-f \f2ltl\f1"
+.BI -f " ltl"
 Translate the LTL formula
 .I ltl
-into a never claim.
+into a
+.I never
+claim.
 .br
 This option reads a formula in LTL syntax from the second argument
-and translates it into Promela syntax (a never claim, which is Promela's
+and translates it into Promela syntax (a
+.I never
+claim, which is Promela's
 equivalent of a Büchi Automaton).
-The LTL operators are written: 
+The LTL operators are written:
 .B []
 (always),
 .B <>
 (eventually),
 and
 .B U
-(strong until).  There is no 
+(strong until).  There is no
 .B X
 (next) operator, to secure
 compatibility with the partial order reduction rules that are
@@ -175,14 +176,16 @@ If the formula contains spaces, it should be quoted to form a
 single argument to the
 .I spin
 command.
-.\"--------------------------F------------
+.
 .TP
-.B "-F \f2file\f1"
+.BI -F " file"
 Translate the LTL formula stored in
 .I file
-into a never claim.
+into a
+.I never
+claim.
 .br
-This behaves identical to option
+This behaves identically to option
 .B -f
 but will read the formula from the
 .I file
@@ -196,64 +199,63 @@ the use of option
 Option
 .B -F
 is meant to solve those problems.)
-.\"--------------------------i------------
+.
 .TP
 .B -i
 Perform an interactive simulation, prompting the user at
 every execution step that requires a nondeterministic choice
 to be made.  The simulation proceeds without user intervention
 when execution is deterministic.
-.\"--------------------------M------------
+.
 .TP
 .B -M
 Produce a message sequence chart in Postscript form for a
 random simulation or a guided simulation
-(when combined with 
+(when combined with
 .BR -t ),
 for the model in
-.I file ,
+.IR file ,
 and write the result into
-.I file.ps .
+.IR file.ps .
 See also option
 .BR -c .
-.\"--------------------------m------------
+.
 .TP
 .B -m
 Changes the semantics of send events.
 Ordinarily, a send action will be (blocked) if the
 target message buffer is full.
 With this option a message sent to a full buffer is lost.
-.\"--------------------------n------------
+.
 .TP
-.B "-n\f2N"
+.BI -n N
 Set the seed for a random simulation to the integer value
-.I N .
+.IR N .
 There is no space between the
 .B -n
 and the integer
 .IR N .
-.\"--------------------------t------------
+.
 .TP
 .B -t
 Perform a guided simulation, following the error trail that
 was produces by an earlier verification run, see the online manuals
 for the details on verification.
-.\"--------------------------V------------
+.
 .TP
 .B -V
 Prints the
 .I spin
 version number and exits.
-.\"--------------------------.------------
-.PD
+.
 .PP
-With only a filename as an argument and no option flags,
+With only a filename as an argument and no options,
 .I spin
 performs a random simulation of the model specified in
 the file (standard input is the default if the filename is omitted).
 If option
 .B -i
-is added, the simulation is 
+is added, the simulation is
 .IR interactive ,
 or if option
 .B -t
@@ -262,21 +264,20 @@ is added, the simulation is
 .PP
 The simulation normally does not generate output, except what is generated
 explicitly by the user within the model with
-.B printf
+.I printf
 statements, and some details about the final state that is
 reached after the simulation completes.
 The group of options
-.B -bglprsv
+.B -bglmprsv
 sets the desired level of information that the user wants
 about a random, guided, or interactive simulation run.
 Every line of output normally contains a reference to the source
 line in the specification that generated it.
-The options are:
-.\"--------------------------bglprsv------------
+.
 .TP
 .B -b
 Suppress the execution of
-.B printf
+.I printf
 statements within the model.
 .TP
 .B -g
@@ -302,30 +303,29 @@ the message type and the message channel number and name.
 Show all message-send events.
 .TP
 .B -v
-Verbose mode, add some more detail, and generat more
+Verbose mode, add some more detail, and generate more
 hints and warnings about the model.
-.PD
 .SH SOURCE
 .B /sys/src/cmd/spin
 .SH SEE ALSO
+.in +4
+.ti -4
+.BR http://spinroot.com :
+.BR GettingStarted.pdf ,
+.BR Roadmap.pdf ,
+.BR Manual.pdf ,
+.BR WhatsNew.pdf ,
+.B Exercises.pdf
+.br
+.in -4
 G.J. Holzmann,
 .IR "Design and Validation of Computer Protocols" ,
 Prentice Hall, 1991.
 .br
-\(em, ``Design and validation of protocols: a tutorial,''
-.I "Computer Networks and ISDN Systems" ,
+—, `Design and validation of protocols: a tutorial,'
+.IR "Computer Networks and ISDN Systems" ,
 Vol. 25, No. 9, 1993, pp. 981-1017.
 .br
-\(em, ``The model checker
-.SM SPIN\c
-\&,''
-.I "IEEE Trans. on Software Engineering" ,
+—, `The model checker Spin,'
+.IR "IEEE Trans. on SE" ,
 Vol, 23, No. 5, May 1997.
-.br
-\(em, ``Using
-.SM SPIN\c
-\&,''
-this manual.
-.PP
-.B http://spinroot.com/
-

sys/src/cmd/spin/README

@@ -2,7 +2,7 @@ the latest version of spin is always
 available via:
 	http://spinroot.com/spin/whatispin.html
 
-to make the sources compile with the mkfile on plan 9
+to make the sources compile with the mkfile on Plan 9
 the following changes were made:
 
 	omitted memory.h from spin.h

sys/src/cmd/spin/dstep.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 #define MAXDSTEP	1024	/* was 512 */
 
@@ -168,7 +164,10 @@ CollectGuards(FILE *fd, Element *e, int inh)
 			break;
 		case ELSE:
 			if (inh++ > 0) fprintf(fd, " || ");
-			fprintf(fd, "(1 /* else */)");
+/* 4.2.5 */		if (Pid != claimnr)
+				fprintf(fd, "(boq == -1 /* else */)");
+			else
+				fprintf(fd, "(1 /* else */)");
 			break;
 		case 'R':
 			if (inh++ > 0) fprintf(fd, " || ");
@@ -387,7 +386,7 @@ putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard)
 			{	sprintf(NextOpt, "goto S_%.3d_%d",
 					e->Seqno, i);
 				NextLab[++Level] = NextOpt;
-				N = (e->n->ntyp == DO) ? e : e->nxt;
+				N = (e->n && e->n->ntyp == DO) ? e : e->nxt;
 				putCode(fd, h->this->frst,
 					h->this->extent, N, 1);
 				Level--;

sys/src/cmd/spin/flow.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern Symbol	*Fname;
 extern int	nr_errs, lineno, verbose;

sys/src/cmd/spin/guided.c

@@ -12,11 +12,7 @@
 #include "spin.h"
 #include <sys/types.h>
 #include <sys/stat.h>
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern RunList	*run, *X;
 extern Element	*Al_El;
@@ -45,7 +41,12 @@ whichproc(int p)
 
 static int
 newer(char *f1, char *f2)
-{	struct stat x, y;
+{
+#if defined(WIN32) || defined(WIN64)
+	struct _stat x, y;
+#else
+	struct stat x, y;
+#endif
 
 	if (stat(f1, (struct stat *)&x) < 0) return 0;
 	if (stat(f2, (struct stat *)&y) < 0) return 1;
@@ -222,7 +223,9 @@ okay:
 				}
 				og = g;
 			} while (g && g != dothis->nxt);
-			X->pc = g?huntele(g, 0, -1):g;
+			if (X != NULL)
+			{	X->pc = g?huntele(g, 0, -1):g;
+			}
 		} else
 		{
 keepgoing:		if (dothis->merge_start)
@@ -230,8 +233,10 @@ keepgoing:		if (dothis->merge_start)
 			else
 				a = dothis->merge;
 
-			X->pc = eval_sub(dothis);
-			if (X->pc) X->pc = huntele(X->pc, 0, a);
+			if (X != NULL)
+			{	X->pc = eval_sub(dothis);
+				if (X->pc) X->pc = huntele(X->pc, 0, a);
+			}
 
 			if (depth >= jumpsteps
 			&& ((verbose&32) || ((verbose&4) && not_claim())))	/* -v or -p */
@@ -247,20 +252,20 @@ keepgoing:		if (dothis->merge_start)
 					if (a && (verbose&32))
 					printf("\t<merge %d now @%d>",
 						dothis->merge,
-						X->pc?X->pc->seqno:-1);
+						(X && X->pc)?X->pc->seqno:-1);
 					printf("\n");
 				}
 				if (verbose&1) dumpglobals();
 				if (verbose&2) dumplocal(X);
 				if (xspin) printf("\n");
 
-				if (!X->pc)
+				if (X && !X->pc)
 				{	X->pc = dothis;
 					printf("\ttransition failed\n");
 					a = 0;	/* avoid inf loop */
 				}
 			}
-			if (a && X->pc && X->pc->seqno != a)
+			if (a && X && X->pc && X->pc->seqno != a)
 			{	dothis = X->pc;
 				goto keepgoing;
 		}	}

sys/src/cmd/spin/main.c

@@ -17,14 +17,11 @@
 #include <time.h>
 #ifdef PC
 #include <io.h>
-#include "y_tab.h"
-
 extern int unlink(const char *);
-
 #else
 #include <unistd.h>
-#include "y.tab.h"
 #endif
+#include "y.tab.h"
 
 extern int	DstepStart, lineno, tl_terse;
 extern FILE	*yyin, *yyout, *tl_out;
@@ -82,7 +79,7 @@ static void	explain(int);
 #ifdef SOLARIS
 #define CPP	"/usr/ccs/lib/cpp"
 #else
-#if defined(__FreeBSD__) || defined(__OpenBSD__)
+#if defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__)
 #define CPP	"cpp"
 #else
 #define CPP	"/bin/cpp"	/* classic Unix systems */
@@ -356,7 +353,7 @@ main(int argc, char *argv[])
 
 		default : usage(); break;
 		}
-		argc--, argv++;
+		argc--; argv++;
 	}
 	if (usedopts && !analyze)
 		printf("spin: warning -o[123] option ignored in simulations\n");
@@ -490,13 +487,6 @@ non_fatal(char *s1, char *s2)
 		printf(s1, s2);
 	else
 		printf(s1);
-#if 0
-	if (yychar != -1 && yychar != 0)
-	{	printf("	saw '");
-		explain(yychar);
-		printf("'");
-	}
-#endif
 	if (yytext && strlen(yytext)>1)
 		printf(" near '%s'", yytext);
 	printf("\n");
@@ -514,6 +504,9 @@ char *
 emalloc(int n)
 {	char *tmp;
 
+	if (n == 0)
+		return NULL;	/* robert shelton 10/20/06 */
+
 	if (!(tmp = (char *) malloc(n)))
 		fatal("not enough memory", (char *)0);
 	memset(tmp, 0, n);
@@ -534,7 +527,7 @@ trapwonly(Lextok *n, char *unused)
 		return;
 
 	if (realread)
-	n->sym->hidden |= 32;	/* var is read at least once */
+	n->sym->hidden |= 128;	/* var is read at least once */
 }
 
 void

sys/src/cmd/spin/mesg.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 #ifndef MAXQ
 #define MAXQ	2500		/* default max # queues  */
@@ -538,11 +534,15 @@ sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q)
 void
 sr_buf(int v, int j)
 {	int cnt = 1; Lextok *n;
-	char lbuf[256];
+	char lbuf[512];
 
 	for (n = Mtype; n && j; n = n->rgt, cnt++)
 		if (cnt == v)
-		{	sprintf(lbuf, "%s", n->lft->sym->name);
+		{	if(strlen(n->lft->sym->name) >= sizeof(lbuf))
+			{	non_fatal("mtype name %s too long", n->lft->sym->name);
+				break;
+			}
+			sprintf(lbuf, "%s", n->lft->sym->name);
 			strcat(Buf, lbuf);
 			return;
 		}
@@ -626,3 +626,19 @@ nochan_manip(Lextok *p, Lextok *n, int d)
 	nochan_manip(p, n->lft, e);
 	nochan_manip(p, n->rgt, 1);
 }
+
+void
+no_internals(Lextok *n)
+{	char *sp;
+
+	if (!n->sym
+	||  !n->sym->name)
+		return;
+
+	sp = n->sym->name;
+
+	if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0)
+	||  (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0))
+	{	fatal("attempt to assign value to system variable %s", sp);
+	}
+}

sys/src/cmd/spin/pangen1.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 #include "pangen1.h"
 #include "pangen3.h"
 
@@ -372,40 +368,53 @@ dolocal(FILE *ofd, char *pre, int dowhat, int p, char *s)
 	Symbol *sp;
 	char buf[64], buf2[128], buf3[128];
 
-	for (j = 0; j < 8; j++)
-	for (h = 0; h <= 1; h++)
-	for (walk = all_names; walk; walk = walk->next)
-	{	sp = walk->entry;
-		if (sp->context
-		&& !sp->owner
-		&&  sp->type == Types[j]
-		&&  ((h == 0 && sp->nel == 1) || (h == 1 && sp->nel > 1))
-		&&  strcmp(s, sp->context->name) == 0)
-		{	switch (dowhat) {
-			case LOGV:
-				if (sp->type == CHAN
-				&&  verbose == 0)
-					break;
-				sprintf(buf, "%s%s:", pre, s);
-				{ sprintf(buf2, "\", ((P%d *)pptr(h))->", p);
-				  sprintf(buf3, ");\n");
+	if (dowhat == INIV)
+	{	/* initialize in order of declaration */
+		for (walk = all_names; walk; walk = walk->next)
+		{	sp = walk->entry;
+			if (sp->context
+			&& !sp->owner
+			&&  strcmp(s, sp->context->name) == 0)
+			{	checktype(sp, s); /* fall through */
+				if (!(sp->hidden&16))
+				{	sprintf(buf, "((P%d *)pptr(h))->", p);
+					do_var(ofd, dowhat, buf, sp, "", " = ", ";\n");
 				}
-				do_var(ofd, dowhat, "", sp, buf, buf2, buf3);
-				break;
-			case INIV:
-				checktype(sp, s); /* fall through */
-				if (sp->hidden&16) { k++; break; }
-			case PUTV:
-				sprintf(buf, "((P%d *)pptr(h))->", p);
-				do_var(ofd, dowhat, buf, sp, "", " = ", ";\n");
 				k++;
-				break;
-			}
-			if (strcmp(s, ":never:") == 0)
-			{	printf("error: %s defines local %s\n",
-					s, sp->name);
-				nr_errs++;
-	}	}	}
+		}	}
+	} else
+	{	for (j = 0; j < 8; j++)
+		for (h = 0; h <= 1; h++)
+		for (walk = all_names; walk; walk = walk->next)
+		{	sp = walk->entry;
+			if (sp->context
+			&& !sp->owner
+			&&  sp->type == Types[j]
+			&&  ((h == 0 && sp->nel == 1) || (h == 1 && sp->nel > 1))
+			&&  strcmp(s, sp->context->name) == 0)
+			{	switch (dowhat) {
+				case LOGV:
+					if (sp->type == CHAN
+					&&  verbose == 0)
+						break;
+					sprintf(buf, "%s%s:", pre, s);
+					{ sprintf(buf2, "\", ((P%d *)pptr(h))->", p);
+					  sprintf(buf3, ");\n");
+					}
+					do_var(ofd, dowhat, "", sp, buf, buf2, buf3);
+					break;
+				case PUTV:
+					sprintf(buf, "((P%d *)pptr(h))->", p);
+					do_var(ofd, dowhat, buf, sp, "", " = ", ";\n");
+					k++;
+					break;
+				}
+				if (strcmp(s, ":never:") == 0)
+				{	printf("error: %s defines local %s\n",
+						s, sp->name);
+					nr_errs++;
+	}	}	}	}
+
 	return k;
 }
 
@@ -472,12 +481,17 @@ c_var(FILE *fd, char *pref, Symbol *sp)
 	case UNSIGNED:
 		sputtype(buf, sp->type);
 		if (sp->nel == 1)
-		fprintf(fd, "\tprintf(\"\t%s %s:\t%%d\\n\", %s%s);\n",
-			buf, sp->name, pref, sp->name);
-		else
-		for (i = 0; i < sp->nel; i++)
-		fprintf(fd, "\tprintf(\"\t%s %s[%d]:\t%%d\\n\", %s%s[%d]);\n",
-			buf, sp->name, i, pref, sp->name, i);
+		{	fprintf(fd, "\tprintf(\"\t%s %s:\t%%d\\n\", %s%s);\n",
+				buf, sp->name, pref, sp->name);
+		} else
+		{	fprintf(fd, "\t{\tint l_in;\n");
+			fprintf(fd, "\t\tfor (l_in = 0; l_in < %d; l_in++)\n", sp->nel);
+			fprintf(fd, "\t\t{\n");
+			fprintf(fd, "\t\t\tprintf(\"\t%s %s[%%d]:\t%%d\\n\", l_in, %s%s[l_in]);\n",
+						buf, sp->name, pref, sp->name);
+			fprintf(fd, "\t\t}\n");
+			fprintf(fd, "\t}\n");
+		}
 		break;
 	case CHAN:
 		if (sp->nel == 1)
@@ -499,6 +513,28 @@ c_var(FILE *fd, char *pref, Symbol *sp)
 	}
 }
 
+int
+c_splurge_any(ProcList *p)
+{	Ordered *walk;
+	Symbol *sp;
+
+	if (strcmp(p->n->name, ":never:") != 0
+	&&  strcmp(p->n->name, ":trace:") != 0
+	&&  strcmp(p->n->name, ":notrace:") != 0)
+	for (walk = all_names; walk; walk = walk->next)
+	{	sp = walk->entry;
+		if (!sp->context
+		||  sp->type == 0
+		||  strcmp(sp->context->name, p->n->name) != 0
+		||  sp->owner || (sp->hidden&1)
+		|| (sp->type == MTYPE && ismtype(sp->name)))
+			continue;
+
+		return 1;
+	}
+	return 0;
+}
+
 void
 c_splurge(FILE *fd, ProcList *p)
 {	Ordered *walk;
@@ -511,6 +547,7 @@ c_splurge(FILE *fd, ProcList *p)
 	for (walk = all_names; walk; walk = walk->next)
 	{	sp = walk->entry;
 		if (!sp->context
+		||  sp->type == 0
 		||  strcmp(sp->context->name, p->n->name) != 0
 		||  sp->owner || (sp->hidden&1)
 		|| (sp->type == MTYPE && ismtype(sp->name)))
@@ -548,7 +585,13 @@ c_wrapper(FILE *fd)	/* allow pan.c to print out global sv entries */
 	{	fprintf(fd, "	case %d:\n", p->tn);
 		fprintf(fd, "	\tprintf(\"local vars proc %%d (%s):\\n\", pid);\n",
 			p->n->name);
-		c_splurge(fd, p);
+		if (c_splurge_any(p))
+		{	fprintf(fd, "	\tprintf(\"local vars proc %%d (%s):\\n\", pid);\n",
+				p->n->name);
+			c_splurge(fd, p);
+		} else
+		{	fprintf(fd, "	\t/* none */\n");
+		}
 		fprintf(fd, "	\tbreak;\n");
 	}
 	fprintf(fd, "	}\n}\n");
@@ -648,16 +691,31 @@ do_var(FILE *ofd, int dowhat, char *s, Symbol *sp,
 				do_init(ofd, sp);
 			fprintf(ofd, "%s", ter);
 		} else
-		for (i = 0; i < sp->nel; i++)
-		{	fprintf(ofd, "\t\t%s%s%s[%d]%s",
-				pre, s, sp->name, i, sep);
-			if (dowhat == LOGV)
-				fprintf(ofd, "%s%s[%d]",
-					s, sp->name, i);
-			else
-				do_init(ofd, sp);
-			fprintf(ofd, "%s", ter);
-		}
+		{	if (sp->ini && sp->ini->ntyp == CHAN)
+			{	for (i = 0; i < sp->nel; i++)
+				{	fprintf(ofd, "\t\t%s%s%s[%d]%s",
+						pre, s, sp->name, i, sep);
+					if (dowhat == LOGV)
+						fprintf(ofd, "%s%s[%d]",
+							s, sp->name, i);
+					else
+						do_init(ofd, sp);
+					fprintf(ofd, "%s", ter);
+				}
+			} else
+			{	fprintf(ofd, "\t{\tint l_in;\n");
+				fprintf(ofd, "\t\tfor (l_in = 0; l_in < %d; l_in++)\n", sp->nel);
+				fprintf(ofd, "\t\t{\n");
+				fprintf(ofd, "\t\t\t%s%s%s[l_in]%s",
+						pre, s, sp->name, sep);
+				if (dowhat == LOGV)
+					fprintf(ofd, "%s%s[l_in]", s, sp->name);
+				else
+					putstmnt(ofd, sp->ini, 0);
+				fprintf(ofd, "%s", ter);
+				fprintf(ofd, "\t\t}\n");
+				fprintf(ofd, "\t}\n");
+		}	}
 		break;
 	}
 }
@@ -753,7 +811,7 @@ tc_predef_np(void)
 {	int i = nrRdy;	/* 1+ highest proctype nr */
 
 	fprintf(th, "#define _NP_	%d\n", i);
-	if (separate == 2) fprintf(th, "extern ");
+/*	if (separate == 2) fprintf(th, "extern ");	*/
 	fprintf(th, "uchar reached%d[3];  /* np_ */\n", i);
 
 	fprintf(th, "#define nstates%d	3 /* np_ */\n", i);
@@ -861,7 +919,7 @@ huntstart(Element *f)
 	Element *elast = (Element *) 0;
 	int cnt = 0;
 
-	while (elast != e && cnt++ < 20)	/* new 4.0.8 */
+	while (elast != e && cnt++ < 200)	/* new 4.0.8 */
 	{	elast = e;
 		if (e->n)
 		{	if (e->n->ntyp == '.' && e->nxt)
@@ -870,7 +928,7 @@ huntstart(Element *f)
 				e = e->sub->this->frst;
 	}	}
 
-	if (cnt >= 20 || !e)
+	if (cnt >= 200 || !e)
 		fatal("confusing control structure", (char *) 0);
 	return e;
 }
@@ -881,7 +939,7 @@ huntele(Element *f, int o, int stopat)
 	int cnt=0; /* a precaution against loops */
 
 	if (e)
-	for (cnt = 0; cnt < 20 && e->n; cnt++)
+	for (cnt = 0; cnt < 200 && e->n; cnt++)
 	{
 		if (e->seqno == stopat)
 			break;
@@ -910,7 +968,7 @@ huntele(Element *f, int o, int stopat)
 			return e;
 		e = g;
 	}
-	if (cnt >= 20 || !e)
+	if (cnt >= 200 || !e)
 		fatal("confusing control structure", (char *) 0);
 	return e;
 }

sys/src/cmd/spin/pangen1.h

@@ -1,6 +1,6 @@
 /***** spin: pangen1.h *****/
 
-/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
+/* Copyright (c) 1989-2005 by Lucent Technologies, Bell Laboratories.     */
 /* All Rights Reserved.  This software is for educational purposes only.  */
 /* No guarantee whatsoever is expressed or implied by the distribution of */
 /* this code.  Permission is given to distribute this code provided that  */
@@ -185,7 +185,7 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"	static char buf[2][2048];",
 	"	int i, toggle = 0;",
 
-	"	if (strlen(s) > 2047) return s;",
+	"	if (!s || strlen(s) > 2047) return s;",
 	"	memset(buf[0], 0, 2048);",
 	"	memset(buf[1], 0, 2048);",
 	"	strcpy(buf[toggle], s);",
@@ -225,7 +225,7 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"	{	printf(\"\\t\\t\");",
 
 	"		q = transmognify(t->tp);",
-	"		for ( ; *q; q++)",
+	"		for ( ; q && *q; q++)",
 	"			if (*q == '\\n')",
 	"				printf(\"\\\\n\");",
 	"			else",
@@ -241,12 +241,12 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"",
 	"	if (wrap_in_progress++) return;",
 	"",
-	"	printf(\"spin: trail ends after %%d steps\\n\", depth);",
+	"	printf(\"spin: trail ends after %%ld steps\\n\", depth);",
 	"	if (onlyproc >= 0)",
 	"	{	if (onlyproc >= now._nr_pr) pan_exit(0);",
 	"		II = onlyproc;",
 	"		z = (P0 *)pptr(II);",
-	"		printf(\"%%3d:\tproc %%d (%%s) \",",
+	"		printf(\"%%3ld:\tproc %%d (%%s) \",",
 	"			depth, II, procname[z->_t]);",
 	"		for (i = 0; src_all[i].src; i++)",
 	"			if (src_all[i].tp == (int) z->_t)",
@@ -265,7 +265,7 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"	if (depth < 0) depth = 0;",
 	"	for (II = 0; II < now._nr_pr; II++)",
 	"	{	z = (P0 *)pptr(II);",
-	"		printf(\"%%3d:\tproc %%d (%%s) \",",
+	"		printf(\"%%3ld:\tproc %%d (%%s) \",",
 	"			depth, II, procname[z->_t]);",
 	"		for (i = 0; src_all[i].src; i++)",
 	"			if (src_all[i].tp == (int) z->_t)",
@@ -293,30 +293,34 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"findtrail(void)",
 	"{	FILE *fd;",
 	"	char fnm[512], *q;",
+	"	char MyFile[512];",
+	"",
+	"	strcpy(MyFile, TrailFile);",	/* avoid problem with non-writable strings */
+	"",
 	"	if (whichtrail)",
-	"	{	sprintf(fnm, \"%%s%%d.%%s\", TrailFile, whichtrail, tprefix);",
+	"	{	sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
 	"		fd = fopen(fnm, \"r\");",
-	"		if (fd == NULL && (q = strchr(TrailFile, \'.\')))",
+	"		if (fd == NULL && (q = strchr(MyFile, \'.\')))",
 	"		{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
-	"			sprintf(fnm, \"%%s%%d.%%s\", TrailFile, whichtrail, tprefix);",
+	"			sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
 	"			*q = \'.\';",
 	"			fd = fopen(fnm, \"r\");",
 	"			if (fd == NULL)",
 	"			{	printf(\"pan: cannot find %%s%%d.%%s or %%s\\n\", ",
-	"					TrailFile, whichtrail, tprefix, fnm);",
+	"					MyFile, whichtrail, tprefix, fnm);",
 	"				pan_exit(1);",
 	"		}	}",
 	"	} else",
-	"	{	sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);",
+	"	{	sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
 	"		fd = fopen(fnm, \"r\");",
-	"		if (fd == NULL && (q = strchr(TrailFile, \'.\')))",
+	"		if (fd == NULL && (q = strchr(MyFile, \'.\')))",
 	"		{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
-	"			sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);",
+	"			sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
 	"			*q = \'.\';",
 	"			fd = fopen(fnm, \"r\");",
 	"			if (fd == NULL)",
 	"			{	printf(\"pan: cannot find %%s.%%s or %%s\\n\", ",
-	"					TrailFile, tprefix, fnm);",
+	"					MyFile, tprefix, fnm);",
 	"				pan_exit(1);",
 	"	}	}	}",
 	"	if (fd == NULL)",
@@ -337,11 +341,16 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"	P0 *z;",
 	"",
 	"	fd = findtrail();	/* exits if unsuccessful */",
-	"	while (fscanf(fd, \"%%d:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
+	"	while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
 	"	{	if (depth == -1)",
 	"			printf(\"<<<<<START OF CYCLE>>>>>\\n\");",
 	"		if (depth < 0)",
 	"			continue;",
+	"		if (i > now._nr_pr)",
+	"		{	printf(\"pan: Error, proc %%d invalid pid \", i);",
+	"			printf(\"transition %%d\\n\", t_id);",
+	"			break;",
+	"		}",
 	"		II = i;",
 	"",
 	"		z = (P0 *)pptr(II);",
@@ -382,7 +391,7 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"			goto moveon;",
 
 	"		if (verbose)",
-	"		{	printf(\"depth: %%3d proc: %%3d trans: %%3d (%%d procs)  \",",
+	"		{	printf(\"depth: %%3ld proc: %%3d trans: %%3d (%%d procs)  \",",
 	"				depth, II, t_id, now._nr_pr);",
 	"			printf(\"forw=%%3d [%%s]\\n\", t->forw, q);",
 	"",
@@ -409,14 +418,14 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"		{",
 	"sameas:		if (no_rck) goto moveon;",
 	"			if (coltrace)",
-	"			{	printf(\"%%d: \", depth);",
+	"			{	printf(\"%%ld: \", depth);",
 	"				for (i = 0; i < II; i++)",
 	"					printf(\"\\t\\t\");",
 	"				printf(\"%%s(%%d):\", procname[z->_t], II);",
-	"				printf(\"[%%s]\\n\", q);",
-	"			} else",
+	"				printf(\"[%%s]\\n\", q?q:\"\");",
+	"			} else if (!silent)",
 	"			{	if (strlen(simvals) > 0) {",
-	"				printf(\"%%3d:	proc %%2d (%%s)\", ",
+	"				printf(\"%%3ld:	proc %%2d (%%s)\", ",
 	"					depth, II, procname[z->_t]);",
 	"				for (i = 0; src_all[i].src; i++)",
 	"					if (src_all[i].tp == (int) z->_t)",
@@ -426,7 +435,7 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"					}",
 	"				printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
 	"				}",
-	"				printf(\"%%3d:	proc %%2d (%%s)\", ",
+	"				printf(\"%%3ld:	proc %%2d (%%s)\", ",
 	"					depth, II, procname[z->_t]);",
 	"				for (i = 0; src_all[i].src; i++)",
 	"					if (src_all[i].tp == (int) z->_t)",
@@ -434,7 +443,7 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"							src_all[i].src[z->_p]);",
 	"						break;",
 	"					}",
-	"				printf(\"(state %%d)\t[%%s]\\n\", z->_p, q);",
+	"				printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");",
 	"				printf(\"\\n\");",
 	"		}	}",
 	"moveon:	z->_p = t->st;",
@@ -491,6 +500,9 @@ static char *Code2a[] = { /* the tail of procedure run() */
 		"#ifdef DEBUG",
 	"	printf(\"New bitstate\\n\");",
 		"#endif",
+	"	if (now._a_t&1)",
+	"	{	nShadow++;",
+	"	}",
 	"	return 0;",
 	"}",
 #endif
@@ -526,6 +538,9 @@ static char *Code2a[] = { /* the tail of procedure run() */
 		"#ifdef DEBUG",
 	"	printf(\"New bitstate\\n\");",
 		"#endif",
+	"	if (now._a_t&1)",
+	"	{	nShadow++;",
+	"	}",
 	"	return 0;",
 	"}",
 	"#endif",
@@ -538,30 +553,35 @@ static char *Code2a[] = { /* the tail of procedure run() */
 	"make_trail(void)",
 	"{	int fd;",
 	"	char *q;",
+	"	char MyFile[512];",
+	"",
+	"	q = strrchr(TrailFile, \'/\');",
+	"	if (q == NULL) q = TrailFile; else q++;",
+	"	strcpy(MyFile, q); /* TrailFile is not a writable string */",
 	"",
 	"	if (iterative == 0 && Nr_Trails++ > 0)",
 	"		sprintf(fnm, \"%%s%%d.%%s\",",
-	"			TrailFile, Nr_Trails-1, tprefix);",
+	"			MyFile, Nr_Trails-1, tprefix);",
 	"	else",
-	"		sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);",
+	"		sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
 	"",
-	"	if ((fd = creat(fnm, (unsigned short) TMODE)) < 0)",
-	"	{	if ((q = strchr(TrailFile, \'.\')))",
+	"	if ((fd = creat(fnm, TMODE)) < 0)",
+	"	{	if ((q = strchr(MyFile, \'.\')))",
 	"		{	*q = \'\\0\';",		/* strip .pml */
 	"			if (iterative == 0 && Nr_Trails-1 > 0)",
 	"				sprintf(fnm, \"%%s%%d.%%s\",",
-	"					TrailFile, Nr_Trails-1, tprefix);",
+	"					MyFile, Nr_Trails-1, tprefix);",
 	"			else",
-	"				sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);",
+	"				sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
 	"			*q = \'.\';",
-	"			fd = creat(fnm, (unsigned short) TMODE);",
+	"			fd = creat(fnm, TMODE);",
 	"	}	}",
 	"	if (fd < 0)",
-	"	{	printf(\"cannot create %%s\\n\", fnm);",
+	"	{	printf(\"pan: cannot create %%s\\n\", fnm);",
 	"		perror(\"cause\");",
 	"	} else",
-	"		printf(\"pan: wrote %%s\\n\", fnm);",
-	"",
+	"	{	printf(\"pan: wrote %%s\\n\", fnm);",
+	"	}",
 	"	return fd;",
 	"}",
 	0
@@ -569,7 +589,7 @@ static char *Code2a[] = { /* the tail of procedure run() */
 
 static char *Code2b[] = {	/* breadth-first search option */
 	"#ifdef BFS",
-	"#define QPROVISO",
+	"#define Q_PROVISO",
 	"#ifndef INLINE_REV",
 	"#define INLINE_REV",
 	"#endif",
@@ -585,8 +605,13 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"	int  sz;",	/* vsize */
 	"	int nrpr;",
 	"	int nrqs;",
-	"	int *po, *ps;",
-	"	int *qo, *qs;",
+	"#if VECTORSZ>32000",
+	"	int *po;",
+	"#else",
+	"	short *po;",
+	"#endif",
+	"	int *qo;",
+	"	uchar *ps, *qs;",
 	"	struct EV_Hold *nxt;",
 	"} EV_Hold;",
 	"",
@@ -594,7 +619,7 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"	Trail	*frame;",
 	"	SV_Hold *onow;",
 	"	EV_Hold *omask;",
-	"#ifdef QPROVISO",
+	"#ifdef Q_PROVISO",
 	"	struct H_el *lstate;",
 	"#endif",
 	"	short boq;",
@@ -647,10 +672,15 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"		&&  (memcmp((char *) Mask, (char *) h->sv, n) == 0)",
 	"		&&  (now._nr_pr == h->nrpr)",
 	"		&&  (now._nr_qs == h->nrqs)",
+	"#if VECTORSZ>32000",
 	"		&&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
-	"		&&  (memcmp((char *) proc_skip,   (char *) h->ps, now._nr_pr * sizeof(int)) == 0)",
 	"		&&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
-	"		&&  (memcmp((char *) q_skip,   (char *) h->qs, now._nr_qs * sizeof(int)) == 0))",
+	"#else",
+	"		&&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)",
+	"		&&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)",
+	"#endif",
+	"		&&  (memcmp((char *) proc_skip,   (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)",
+	"		&&  (memcmp((char *) q_skip,   (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))",
 	"			break;",
 	"	if (!h)",
 	"	{	h = (EV_Hold *) emalloc(sizeof(EV_Hold));",
@@ -664,14 +694,22 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"		if (now._nr_pr > 0)",
 	"		{	h->po = (int *) emalloc(now._nr_pr * sizeof(int));",
 	"			h->ps = (int *) emalloc(now._nr_pr * sizeof(int));",
+	"#if VECTORSZ>32000",
 	"			memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));",
-	"			memcpy((char *) h->ps, (char *) proc_skip,   now._nr_pr * sizeof(int));",
+	"#else",
+	"			memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));",
+	"#endif",
+	"			memcpy((char *) h->ps, (char *) proc_skip,   now._nr_pr * sizeof(uchar));",
 	"		}",
 	"		if (now._nr_qs > 0)",
 	"		{	h->qo = (int *) emalloc(now._nr_qs * sizeof(int));",
 	"			h->qs = (int *) emalloc(now._nr_qs * sizeof(int));",
+	"#if VECTORSZ>32000",
 	"			memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));",
-	"			memcpy((char *) h->qs, (char *) q_skip,   now._nr_qs * sizeof(int));",
+	"#else",
+	"			memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));",
+	"#endif",
+	"			memcpy((char *) h->qs, (char *) q_skip,   now._nr_qs * sizeof(uchar));",
 	"		}",
 	"",
 	"		h->nxt = kept;",
@@ -725,7 +763,7 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"	t->onow = getsv(vsize);",
 	"	memcpy((char *)t->onow->sv, (char *)&now, vsize);",
 	"	t->omask = getsv_mask(vsize);",
-	"#if defined(FULLSTACK) && defined(QPROVISO)",
+	"#if defined(FULLSTACK) && defined(Q_PROVISO)",
 	"	t->lstate = Lstate;",
 	"#endif",
 	"	if (!bfs_bot)",
@@ -750,7 +788,7 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"	bfs_trail = t->nxt;",
 	"	if (!bfs_trail)",
 	"		bfs_bot = (BFS_Trail *) 0;",
-	"#if defined(QPROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
+	"#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
 	"	if (t->lstate) t->lstate->tagged = 0;",
 	"#endif",
 	"",
@@ -764,12 +802,20 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"	memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",
 
 	"	if (now._nr_pr > 0)",
+	"#if VECTORSZ>32000",
 	"	{	memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));",
-	"		memcpy((char *)proc_skip,   (char *)t->omask->ps, now._nr_pr * sizeof(int));",
+	"#else",
+	"	{	memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));",
+	"#endif",
+	"		memcpy((char *)proc_skip,   (char *)t->omask->ps, now._nr_pr * sizeof(uchar));",
 	"	}",
 	"	if (now._nr_qs > 0)",
+	"#if VECTORSZ>32000",
 	"	{	memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));",
-	"		memcpy((uchar *)q_skip,   (uchar *)t->omask->qs, now._nr_qs * sizeof(int));",
+	"#else",
+	"	{	memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));",
+	"#endif",
+	"		memcpy((uchar *)q_skip,   (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));",
 	"	}",
 
 	"	freesv(t->onow);	/* omask not freed */",
@@ -867,7 +913,7 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"			} else",
 	"			{	truncs++;",
 
-	"#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(QPROVISO)",
+	"#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(Q_PROVISO)",
 		"#if !defined(QLIST) && !defined(BITSTATE)",
 	"				if (Lstate && Lstate->tagged) trpt->tau |= 64;",
 		"#else",
@@ -893,9 +939,11 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"#endif",
 	"}",
 	"",
+	"Trail *ntrpt;",	/* 4.2.8 */
+	"",
 	"void",
 	"bfs(void)",
-	"{	Trans *t; Trail *ntrpt, *otrpt, *x;",
+	"{	Trans *t; Trail *otrpt, *x;",
 	"	uchar _n, _m, ot, nps = 0;",
 	"	int tt, E_state;",
 	"	short II, From = (short) (now._nr_pr-1), To = BASE;",
@@ -1199,13 +1247,15 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"		j = strlen(snap);",
 	"		if (write(fd, snap, j) != j)",
 	"		{       printf(\"pan: error writing %%s\\n\", fnm);",
-	"			exit(1);",
+	"			pan_exit(1);",
 	"	}	}",
 	"}",
 	"",
 	"void",
 	"nuerror(char *str)",
 	"{	int fd = make_trail();",
+	"	int j;",
+	"",
 	"	if (fd < 0) return;",
 	"#ifdef VERI",
 	"	sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
@@ -1217,9 +1267,19 @@ static char *Code2b[] = {	/* breadth-first search option */
 	"#endif",
 	"	trcnt = 1;",
 	"	putter(trpt, fd);",
+	"	if (ntrpt->o_t)",	/* 4.2.8 -- Alex example, missing last transition */
+	"	{	sprintf(snap, \"%%d:%%d:%%d\\n\",",
+	"			trcnt++, ntrpt->pr, ntrpt->o_t->t_id);",
+	"		j = strlen(snap);",
+	"		if (write(fd, snap, j) != j)",
+	"		{       printf(\"pan: error writing %%s\\n\", fnm);",
+	"			pan_exit(1);",
+	"	}	}",
 	"	close(fd);",
 	"	if (errors >= upto && upto != 0)",
+	"	{",
 	"		wrapup();",
+	"	}",
 	"}",
 	"#endif",	/* BFS */
 	0,
@@ -1398,7 +1458,7 @@ static char *Code2c[] = {
 	"#endif",
 	"	}",
 	"#ifdef NEGATED_TRACE",
-	"	now._event = start_event; /* only 1st try will count */",
+	"	now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */",
 	"#else",	
 		"#ifndef BFS",
 	"	depth++; trpt++;",
@@ -1456,7 +1516,7 @@ static char *Code2c[] = {
 	"stack2disk(void)",
 	"{",
 	"	if (!stackwrite",
-	"	&&  (stackwrite = creat(stackfile, 0666)) < 0)",
+	"	&&  (stackwrite = creat(stackfile, TMODE)) < 0)",
 	"		Uerror(\"cannot create stackfile\");",
 	"",
 	"	if (write(stackwrite, trail, DDD*sizeof(Trail))",
@@ -1563,7 +1623,8 @@ static char *Code2c[] = {
 	"	}",
 	"AllOver:",
 	"#if defined(FULLSTACK) && !defined(MA)",
-	"	trpt->ostate = (struct H_el *) 0;",
+	"	/* if atomic or rv move, carry forward previous state */",
+	"	trpt->ostate = (trpt-1)->ostate;",	/* was: = (struct H_el *) 0;*/
 	"#endif",
 	"#ifdef VERI",
 	"	if ((trpt->tau&4) || ((trpt-1)->tau&128))",
@@ -1628,8 +1689,22 @@ static char *Code2c[] = {
 		"#endif",
 	"#endif",
 	"			kk = (II == 1 || II == 2);",
-
+				/* II==0 new state */
+				/* II==1 old state */
+				/* II==2 on current dfs stack */
+				/* II==3 on 1st dfs stack */
 	"#ifndef SAFETY",
+
+	"			if (!fairness && a_cycles)",
+	"			if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))",
+	"			{	II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */",
+		"#ifdef VERBOSE",
+	"				printf(\"state match on dfs stack\\n\");",
+		"#endif",
+	"				goto same_case;",
+	"			}",
+
+
 		"#if defined(FULLSTACK) && defined(BITSTATE)",
 	"			if (!JJ && (now._a_t&1) && depth > A_depth)",
 	"			{	int oj1 = j1;",
@@ -1657,12 +1732,10 @@ static char *Code2c[] = {
 	"			   } else",
 		"#endif",
 	"			   {",
-		"#ifdef BITSTATE",
-	"				depthfound = Lstate->tagged - 1;",
-		"#else",
-	"				depthfound = depth_of(Lstate);",
+		"#ifndef BITSTATE",
 	"				nShadow--;",
 		"#endif",
+	"same_case:			if (Lstate) depthfound = Lstate->D;",
 		"#ifdef NP",
 	"				uerror(\"non-progress cycle\");",
 		"#else",
@@ -2736,7 +2809,6 @@ static char *Code2c[] = {
 	"#endif",
 	"#endif",
 
-
 	"	signal(SIGINT, SIG_DFL);",
 	"	printf(\"(%%s)\\n\", Version);",
 	"	if (!done) printf(\"Warning: Search not completed\\n\");",
@@ -2750,7 +2822,7 @@ static char *Code2c[] = {
 	"	printf(\"	+ Partial Order Reduction\\n\");",
 	"#endif",
 #if 0
-	"#ifdef QPROVISO",
+	"#ifdef Q_PROVISO",
 	"	printf(\"	+ Queue Proviso\\n\");",
 	"#endif",
 #endif
@@ -2925,7 +2997,7 @@ static char *Code2c[] = {
 	"		{	printf(\"\tState-vector as stored = %%.0f byte\",",
 	"			(tmp_nr)/(nstates-nShadow) -",
 	"			(double) (sizeof(struct H_el) - sizeof(unsigned)));",
-	"			printf(\" + %%d byte overhead\\n\",",
+	"			printf(\" + %%ld byte overhead\\n\",",
 	"			sizeof(struct H_el)-sizeof(unsigned));",
 	"		}",
 			"#endif",
@@ -2936,8 +3008,9 @@ static char *Code2c[] = {
 			"#endif",
 		"#endif",
 		"#ifndef BFS",
-	"		printf(\"%%-6.3f\tmemory used for DFS stack (-m%%d)\\n\",",
+	"		printf(\"%%-6.3f\tmemory used for DFS stack (-m%%ld)\\n\",",
 	"			nr2/1000000., maxdepth);",
+	"		remainder = remainder - nr2;",
 		"#endif",
 	"		if (remainder - fragment > 0.0)",
 	"		printf(\"%%-6.3f\tother (proc and chan stacks)\\n\",",
@@ -2986,13 +3059,14 @@ static char *Code2c[] = {
 	"stopped(int arg)",
 	"{	printf(\"Interrupted\\n\");",
 	"	wrapup();",
+	"	pan_exit(0);",
 	"}",
 	"/*",
 	" * based on Bob Jenkins hash-function from 1996",
 	" * see: http://www.burtleburtle.net/bob/",
 	" */",
 	"",
-"#ifdef HASH64",
+"#if defined(HASH64) || defined(WIN64)",
 	/* 64-bit Jenkins hash: http://burtleburtle.net/bob/c/lookup8.c */
 	"#define mix(a,b,c) \\",
 	"{ a -= b; a -= c; a ^= (c>>43); \\",
@@ -3148,6 +3222,7 @@ static char *Code2c[] = {
 	"		case 'P': readtrail = 1; onlyproc = atoi(&argv[1][2]); break;",
 	"		case 'C': coltrace = 1; goto samething;",
 	"		case 'g': gui = 1; goto samething;",
+	"		case 'S': silent = 1; break;",
 	"#endif",
 	"		case 'R': Nrun = atoi(&argv[1][2]); break;",
 	"#ifdef BITSTATE",
@@ -3161,10 +3236,20 @@ static char *Code2c[] = {
 	"		case 'w': ssize = atoi(&argv[1][2]); break;",
 	"		case 'Y': signoff = 1; break;",
 	"		case 'X': efd = stdout; break;",
-	"		default : usage(efd); break;",
+	"		default : fprintf(efd, \"saw option -%%c\\n\", argv[1][1]); usage(efd); break;",
 	"		}",
 	"		argc--; argv++;",
 	"	}",
+	"	if (iterative && TMODE != 0666)",
+	"	{	TMODE = 0666;",
+	"		fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
+	"	}",
+	"#if defined(WIN32) || defined(WIN64)",
+	"	if (TMODE == 0666)",
+	"		TMODE = _S_IWRITE | _S_IREAD;",
+	"	else",
+	"		TMODE = _S_IREAD;",
+	"#endif",
 	"#ifdef OHASH",
 	"	fprintf(efd, \"warning: -DOHASH no longer supported (directive ignored)\\n\");",
 	"#endif",
@@ -3208,10 +3293,6 @@ static char *Code2c[] = {
 	"	}",
 
 	"#endif",
-	"	if (iterative && TMODE != 0666)",
-	"	{	TMODE = 0666;",
-	"		fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
-	"	}",
 	"#ifdef SC",
 	"	hiwater = HHH = maxdepth-10;",
 	"	DDD = HHH/2;",
@@ -3375,14 +3456,18 @@ static char *Code2c[] = {
 	"#endif",
 
 	"#if SYNC>0 && !defined(NOREDUCE)",
-	"#ifdef HAS_UNLESS",
+		"#ifdef HAS_UNLESS",
 	"	fprintf(efd, \"warning: use of a rendezvous stmnts in the escape\\n\");",
 	"	fprintf(efd, \"\tof an unless clause, if present, could make p.o. reduction\\n\");",
 	"	fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");",
-	"#ifdef BFS",
+			"#ifdef BFS",
 	"	fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");",
+			"#endif",
+		"#endif",
 	"#endif",
-	"#endif",
+	"#if SYNC>0 && defined(BFS)",
+	"	fprintf(efd, \"warning: use of rendezvous in BFS mode \");",
+	"	fprintf(efd, \"does not preserve all invalid endstates\\n\");",
 	"#endif",
 	"#if !defined(REACH) && !defined(BITSTATE)",
 	"	if (iterative != 0 && a_cycles == 0)",
@@ -3467,7 +3552,7 @@ static char *Code2c[] = {
 	"		nmask = mask;",
 	"#endif",
 	"	} else if (WS != 4)",
-	"	{	fprintf(stderr, \"pan: wordsize %%d not supported\\n\", WS);",
+	"	{	fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", WS);",
 	"		exit(1);",
 	"	} else	/* WS == 4 and ssize < 32 */",
 	"	{	mask = ((1L<<ssize)-1);	/* hash init */",
@@ -3564,6 +3649,7 @@ static char *Code2c[] = {
 	"	fprintf(fd, \"\t-C  read and execute trail - columnated output (can add -v,-n)\\n\");",
 	"	fprintf(fd, \"\t-PN read and execute trail - restrict trail output to proc N\\n\");",
 	"	fprintf(fd, \"\t-g  read and execute trail + msc gui support\\n\");",
+	"	fprintf(fd, \"\t-S  silent replay: only user defined printfs show\\n\");",
 	"#endif",
 	"#ifdef BITSTATE",
 	"	fprintf(fd, \"\t-RN repeat run Nx with N \");",
@@ -3574,9 +3660,9 @@ static char *Code2c[] = {
 	"	fprintf(fd, \"\t-tsuf replace .trail with .suf on trailfiles\\n\");",
 	"	fprintf(fd, \"\t-V  print SPIN version number\\n\");",
 	"	fprintf(fd, \"\t-v  verbose -- filenames in unreached state listing\\n\");",
-	"	fprintf(fd, \"\t-wN hashtable of 2^N entries\");",
+	"	fprintf(fd, \"\t-wN hashtable of 2^N entries \");",
 	"	fprintf(fd, \"(defaults to -w%%d)\\n\", ssize);",
-	"	pan_exit(1);",
+	"	exit(1);",
 	"}",
 	"",
 	"char *",
@@ -3782,7 +3868,7 @@ static char *Code2c[] = {
 	"",
 	"	if (unwinding) return; /* 1.4.2 */",
 	"	if (strncmp(str, laststr, 254))",
-	"	printf(\"pan: %%s (at depth %%d)\\n\", str,",
+	"	printf(\"pan: %%s (at depth %%ld)\\n\", str,",
 	"		(depthfound==-1)?depth:depthfound);",
 	"	strncpy(laststr, str, 254);",
 	"	errors++;",
@@ -3827,7 +3913,7 @@ static char *Code2c[] = {
 	"	if (iterative != 0 && maxdepth > 0)",
 	"	{	maxdepth = (iterative == 1)?(depth-1):(depth/2);",
 	"		warned = 1;",
-	"		printf(\"pan: reducing search depth to %%d\\n\",",
+	"		printf(\"pan: reducing search depth to %%ld\\n\",",
 	"			maxdepth);",
 	"	} else",
 "#endif",
@@ -3837,7 +3923,7 @@ static char *Code2c[] = {
 	"}\n",
 	"int",
 	"xrefsrc(int lno, S_F_MAP *mp, int M, int i)",
-	"{	Trans *T; int j;",
+	"{	Trans *T; int j, retval=1;",
 	"	for (T = trans[M][i]; T; T = T->nxt)",
 	"	if (T && T->tp)",
 	"	{	if (strcmp(T->tp, \".(goto)\") == 0",
@@ -3855,12 +3941,13 @@ static char *Code2c[] = {
 	"		if (strcmp(T->tp, \"\") != 0)",
 	"		{	char *q;",
 	"			q = transmognify(T->tp);",
-	"			printf(\", \\\"%%s\\\"\", q);",
+	"			printf(\", \\\"%%s\\\"\", q?q:\"\");",
 	"		} else if (stopstate[M][i])",
 	"			printf(\", -end state-\");",
 	"		printf(\"\\n\");",
+	"		retval = 0; /* reported */",
 	"	}",
-	"	return 0;",
+	"	return retval;",
 	"}\n",
 	"void",
 	"r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)",
@@ -3886,7 +3973,9 @@ static char *Code2c[] = {
 	"putrail(void)",
 	"{	int fd; long i, j;",
 	"	Trail *trl;",
+	"#if defined VERI || defined(MERGED)",
 	"	char snap[64];",
+	"#endif",
 	"",
 	"	fd = make_trail();",
 	"	if (fd < 0) return;",
@@ -3904,7 +3993,7 @@ static char *Code2c[] = {
 	"		trl = getframe(i);",
 	"		if (!trl->o_t) continue;",
 	"		if (trl->o_pm&128) continue;",
-	"		sprintf(snap, \"%%d:%%d:%%d\\n\", ",
+	"		sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
 	"			i, trl->pr, trl->o_t->t_id);",
 	"		j = strlen(snap);",
 	"		if (write(fd, snap, j) != j)",
@@ -3970,7 +4059,7 @@ static char *Code2c[] = {
 	"p_restor(int h)",
 	"{	int i; char *z = (char *) &now;\n",
 	"	proc_offset[h] = stack->o_offset;",
-	"	proc_skip[h]   = stack->o_skip;",
+	"	proc_skip[h]   = (uchar) stack->o_skip;",
 	"#ifndef XUSAFE",
 	"	p_name[h] = stack->o_name;",
 	"#endif",
@@ -4009,7 +4098,7 @@ static char *Code2c[] = {
 	"	int k, k_end;",
 	"#endif",
 	"	q_offset[now._nr_qs] = stack->o_offset;",
-	"	q_skip[now._nr_qs]   = stack->o_skip;",
+	"	q_skip[now._nr_qs]   = (uchar) stack->o_skip;",
 	"#ifndef XUSAFE",
 	"	q_name[now._nr_qs]   = stack->o_name;",
 	"#endif",
@@ -4092,7 +4181,11 @@ static char *Code2c[] = {
 	"		}",
 	"		stack = stack->nxt;",
 	"		stack->o_offset = proc_offset[h];",
-	"		stack->o_skip   = proc_skip[h];",
+	"#if VECTORSZ>32000",
+	"		stack->o_skip   = (int) proc_skip[h];",
+	"#else",
+	"		stack->o_skip   = (short) proc_skip[h];",
+	"#endif",
 	"#ifndef XUSAFE",
 	"		stack->o_name   = p_name[h];",
 	"#endif",
@@ -4103,7 +4196,7 @@ static char *Code2c[] = {
 	"	vsize = proc_offset[h];",
 	"	now._nr_pr = now._nr_pr - 1;",
 	"	memset((char *)pptr(h), 0, d);",
-	"	vsize -= proc_skip[h];",
+	"	vsize -= (int) proc_skip[h];",
 	"#ifndef NOVSZ",
 	"	now._vsz = vsize;",
 	"#endif",
@@ -4131,7 +4224,11 @@ static char *Code2c[] = {
 	"		}",
 	"		stack = stack->nxt;",
 	"		stack->o_offset = q_offset[h];",
-	"		stack->o_skip   = q_skip[h];",
+	"#if VECTORSZ>32000",
+	"		stack->o_skip   = (int) q_skip[h];",
+	"#else",
+	"		stack->o_skip   = (short) q_skip[h];",
+	"#endif",
 	"#ifndef XUSAFE",
 	"		stack->o_name   = q_name[h];",
 	"#endif",
@@ -4141,7 +4238,7 @@ static char *Code2c[] = {
 	"	vsize = q_offset[h];",
 	"	now._nr_qs = now._nr_qs - 1;",
 	"	memset((char *)qptr(h), 0, d);",
-	"	vsize -= q_skip[h];",
+	"	vsize -= (int) q_skip[h];",
 	"#ifndef NOVSZ",
 	"	now._vsz = vsize;",
 	"#endif",
@@ -4218,7 +4315,6 @@ static char *Code2c[] = {
 	"	memcpy((char *)&A_Root, (char *)&now, vsize);",
 	"	A_depth = depthfound = depth;",
 	"	new_state();	/* start 2nd DFS */",
-
 	"	now._a_t = o_a_t;",
 	"#ifndef NOFAIR",
 	"	now._cnt[1] = o_cnt;",
@@ -4240,13 +4336,7 @@ static char *Code2c[] = {
 	"struct H_el *Free_list = (struct H_el *) 0;",
 	"void",
 	"onstack_init(void)	/* to store stack states in a bitstate search */",
-	"{	S_Tab = (struct H_el **)",
-#if 0
-	"		emalloc((1L<<(ssize-3))*sizeof(struct H_el *));",
-			/* can lead to excessive memory use */
-#else
-	"		emalloc(maxdepth*sizeof(struct H_el *));",
-#endif
+	"{	S_Tab = (struct H_el **) emalloc(maxdepth*sizeof(struct H_el *));",
 	"}",
 	"struct H_el *",
 	"grab_state(int n)",
@@ -4582,7 +4672,7 @@ static char *Code2c[] = {
 	"	for (w = Free_list; w; Fa++, last=w, w = w->nxt)",
 	"	{	if ((int) w->tagged <= n)",
 	"		{	if (last)",
-	"			{	v->nxt = w->nxt;",
+	"			{	v->nxt = w; /* was: v->nxt = w->nxt; */",
 	"				last->nxt = v;",
 	"			} else",
 	"			{	v->nxt = Free_list;",
@@ -4635,7 +4725,7 @@ static char *Code2c[] = {
 	"	for (tmp = S_Tab[j1]; tmp; Zn++, tmp = tmp->nxt)",
 	"	{	m = memcmp(((char *)&(tmp->state)),v,n);",
 	"		if (m <= 0)",
-	"		{	Lstate = tmp;",
+	"		{	Lstate = (struct H_el *) tmp;",
 	"			break;",
 	"	}	}",
 	"	PROBE++;",
@@ -4787,6 +4877,9 @@ static char *Code2c[] = {
 	"hstore(char *vin, int nin)	/* hash table storage */",
 	"{	struct H_el *tmp, *ntmp, *olst = (struct H_el *) 0;",
 	"	char *v; int n, m=0;",
+	"#ifdef HC",
+	"	uchar rem_a;",
+	"#endif",
 	"#ifdef NOCOMP",	/* defined by BITSTATE */
 		"#if defined(BITSTATE) && defined(LC)",
 	"	if (S_Tab == H_tab)",
@@ -4800,7 +4893,14 @@ static char *Code2c[] = {
 		"#endif",
 	"#else",
 	"	v = (char *) &comp_now;",
+	"	#ifdef HC",
+	"	rem_a = now._a_t;",	/* 4.3.0 */
+	"	now._a_t = 0;",	/* for hashing/state matching to work right */
+	"	#endif",
 	"	n = compress(vin, nin);", /* with HC, this calls s_hash */
+	"	#ifdef HC",
+	"	now._a_t = rem_a;",	/* 4.3.0 */
+	"	#endif",
 		"#ifndef SAFETY",
 	"	if (S_A)",
 	"	{	v[0] = 0;	/* _a_t  */",
@@ -4874,7 +4974,7 @@ static char *Code2c[] = {
 	"#ifdef FULLSTACK",
 		"#ifndef SAFETY",	/* or else wasnew == 0 */
 	"		if (wasnew)",
-	"		{	Lstate = tmp;",
+	"		{	Lstate = (struct H_el *) tmp;",
 	"			tmp->tagged |= V_A;",
 	"			if ((now._a_t&1)",
 	"			&& (tmp->tagged&A_V)",
@@ -4897,7 +4997,7 @@ static char *Code2c[] = {
 	"		} else",
 		"#endif",
 	"		if ((S_A)?(tmp->tagged&V_A):tmp->tagged)",
-	"		{	Lstate = tmp;",
+	"		{	Lstate = (struct H_el *) tmp;",
 		"#ifndef SAFETY",
 	"			/* already on current dfs stack */",
 	"			/* but may also be on 1st dfs stack */",
@@ -4962,8 +5062,8 @@ static char *Code2c[] = {
 	"			return 0;",
 	"		}",
 	"#endif",
-	"#if defined(BFS) && defined(QPROVISO)",
-	"		Lstate = tmp;",
+	"#if defined(BFS) && defined(Q_PROVISO)",
+	"		Lstate = (struct H_el *) tmp;",
 	"#endif",
 	"		return 1; /* match outside stack */",
 	"	       } else if (m < 0)",
@@ -4994,7 +5094,7 @@ static char *Code2c[] = {
 	"	printf(\"	New state %%d\\n\", (int) nstates);",
 		"#endif",
 	"#endif",
-	"#ifdef REACH",
+	"#if !defined(SAFETY) || defined(REACH)",
 	"	tmp->D = depth;",
 	"#endif",
 	"#ifndef SAFETY",
@@ -5022,7 +5122,7 @@ static char *Code2c[] = {
 		"#ifdef DEBUG",
 	"	dumpstate(-1, v, n, tmp->tagged);",
 		"#endif",
-	"	Lstate = tmp;",
+	"	Lstate = (struct H_el *) tmp;",
 	"#else",
 		"#ifdef DEBUG",
 	"	dumpstate(-1, v, n, 0);",

sys/src/cmd/spin/pangen2.c

@@ -11,11 +11,7 @@
 
 #include "spin.h"
 #include "version.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 #include "pangen2.h"
 #include "pangen4.h"
 #include "pangen5.h"
@@ -186,15 +182,15 @@ gensrc(void)
 	fprintf(th, "#define uint	unsigned int\n");
 	fprintf(th, "#endif\n");
 
-	if (sizeof(long) > 4)	/* 64 bit machine */
+	if (sizeof(void *) > 4)	/* 64 bit machine */
 	{	fprintf(th, "#ifndef HASH32\n");
 		fprintf(th, "#define HASH64\n");
 		fprintf(th, "#endif\n");
 	}
-
+#if 0
 	if (sizeof(long)==sizeof(int))
 		fprintf(th, "#define long	int\n");
-
+#endif
 	if (separate == 1 && !claimproc)
 	{	Symbol *n = (Symbol *) emalloc(sizeof(Symbol));
 		Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
@@ -314,6 +310,8 @@ doless:
 
 	if (separate != 2)
 		ntimes(tc, 0, 1, Preamble);
+	else
+		fprintf(tc, "extern int verbose; extern long depth;\n");
 
 	fprintf(tc, "#ifndef NOBOUNDCHECK\n");
 	fprintf(tc, "#define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n");
@@ -408,6 +406,7 @@ doless:
 	for (p = rdy; p; p = p->nxt)
 		putproc(p);
 
+
 	if (separate != 2)
 	{	fprintf(th, "struct {\n");
 		fprintf(th, "	int tp; short *src;\n");
@@ -417,6 +416,9 @@ doless:
 				p->tn, p->tn);
 		fprintf(th, "	{ 0, (short *) 0 }\n");
 		fprintf(th, "};\n");
+		fprintf(th, "short *frm_st0;\n");	/* records src states for transitions in never claim */
+	} else
+	{	fprintf(th, "extern short *frm_st0;\n");
 	}
 
 	gencodetable(th);
@@ -472,8 +474,12 @@ doless:
 		fprintf(th, "#define REVERSE_MOVES\t\"pan_t.b\"\n");
 		fprintf(th, "#define TRANSITIONS\t\"pan_t.t\"\n");
 		fprintf(tc, "extern int Maxbody;\n");
+		fprintf(tc, "#if VECTORSZ>32000\n");
 		fprintf(tc, "extern int proc_offset[];\n");
-		fprintf(tc, "extern int proc_skip[];\n");
+		fprintf(tc, "#else\n");
+		fprintf(tc, "extern short proc_offset[];\n");
+		fprintf(tc, "#endif\n");
+		fprintf(tc, "extern uchar proc_skip[];\n");
 		fprintf(tc, "extern uchar *reached[];\n");
 		fprintf(tc, "extern uchar *accpstate[];\n");
 		fprintf(tc, "extern uchar *progstate[];\n");
@@ -714,7 +720,12 @@ putproc(ProcList *p)
 	if (Pid == claimnr
 	&&  separate == 1)
 	{	fprintf(th, "extern uchar reached%d[];\n", Pid);
+#if 0
 		fprintf(th, "extern short nstates%d;\n", Pid);
+#else
+		fprintf(th, "\n#define nstates%d	%d\t/* %s */\n",
+			Pid, p->s->maxel, p->n->name);
+#endif
 		fprintf(th, "extern short src_ln%d[];\n", Pid);
 		fprintf(th, "extern S_F_MAP src_file%d[];\n", Pid);
 		fprintf(th, "#define endstate%d	%d\n",
@@ -731,7 +742,7 @@ putproc(ProcList *p)
 
 	AllGlobal = (p->prov)?1:0;	/* process has provided clause */
 
-	fprintf(th, "\nshort nstates%d=%d;\t/* %s */\n",
+	fprintf(th, "\n#define nstates%d	%d\t/* %s */\n",
 		Pid, p->s->maxel, p->n->name);
 	if (Pid == claimnr)
 	fprintf(th, "#define nstates_claim	nstates%d\n", Pid);
@@ -826,7 +837,8 @@ hidden(Lextok *n)
 static int
 getNid(Lextok *n)
 {
-	if (n->sym->type == STRUCT
+	if (n->sym
+	&&  n->sym->type == STRUCT
 	&&  n->rgt && n->rgt->lft)
 		return getNid(n->rgt->lft);
 
@@ -1470,6 +1482,22 @@ case_cache(Element *e, int a)
 	memset(CnT, 0, sizeof(CnT));
 	YZmax = YZcnt = 0;
 
+/* NEW 4.2.6 */
+	if (Pid == claimnr)
+	{
+		fprintf(tm, "\n#if defined(VERI) && !defined(NP)\n\t\t");
+		fprintf(tm, "{	static int reported%d = 0;\n\t\t", e->seqno);
+		/* source state changes in retrans and must be looked up in frm_st0[t->forw] */
+		fprintf(tm, "	if (verbose && !reported%d)\n\t\t", e->seqno);
+		fprintf(tm, "	{	printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",\n\t\t");
+		fprintf(tm, "			depth, frm_st0[t->forw], src_claim[%d]);\n\t\t", e->seqno);
+		fprintf(tm, "		reported%d = 1;\n\t\t", e->seqno);
+		fprintf(tm, "		fflush(stdout);\n\t\t");
+		fprintf(tm, "}	}\n");
+		fprintf(tm, "#endif\n\t\t");
+	}
+/* end */
+
 	/* the src xrefs have the numbers in e->seqno builtin */
 	fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, e->seqno);
 
@@ -1838,7 +1866,9 @@ find_target(Element *e)
 		break;
 	case BREAK:
 		if (e->nxt)
-		f = find_target(huntele(e->nxt, e->status, -1));
+		{	f = find_target(huntele(e->nxt, e->status, -1));
+			break;	/* 4.3.0 -- was missing */
+		}
 		/* else fall through */
 	default:
 		f = e;
@@ -1867,13 +1897,19 @@ scan_seq(Sequence *s)
 		||  has_global(f->n))
 			return 1;
 		if (f->n->ntyp == GOTO)	/* may reach other atomic */
-		{	g = target(f);
+		{
+#if 0
+			/* if jumping from an atomic without globals into
+			 * one with globals, this does the wrong thing
+			 * example by Claus Traulsen, 22 June 2007
+			 */
+			g = target(f);
 			if (g
 			&& !(f->status & L_ATOM)
 			&& !(g->status & (ATOM|L_ATOM)))
-			{	fprintf(tt, "	/* goto mark-down, ");
-				fprintf(tt, "line %d - %d */\n",
-					f->n->ln, (g->n)?g->n->ln:0);
+#endif
+			{	fprintf(tt, "	/* mark-down line %d */\n",
+					f->n->ln);
 				return 1; /* assume worst case */
 		}	}
 		for (h = f->sub; h; h = h->nxt)
@@ -2055,9 +2091,10 @@ putstmnt(FILE *fd, Lextok *now, int m)
 		for (v = now->lft, i = 0; v; v = v->rgt, i++)
 		{	cat2(", ", v->lft);
 		}
+		check_param_count(i, now);
 
 		if (i > Npars)
-		{	printf("	%d parameters used, %d expected\n", i, Npars);
+		{	printf("\t%d parameters used, max %d expected\n", i, Npars);
 			fatal("too many parameters in run %s(...)",
 			now->sym->name);
 		}
@@ -2703,7 +2740,11 @@ putstmnt(FILE *fd, Lextok *now, int m)
 	case C_EXPR:
 		fprintf(fd, "(");
 		plunk_expr(fd, now->sym->name);
+#if 1
+		fprintf(fd, ")");
+#else
 		fprintf(fd, ") /* %s */ ", now->sym->name);
+#endif
 		break;
 
 	case C_CODE:
@@ -2944,3 +2985,12 @@ count_runs(Lextok *n)
 	if (runcount == 1 && opcount > 1)
 		fatal("use of run operator in compound expression", "");
 }
+
+void
+any_runs(Lextok *n)
+{
+	runcount = opcount = 0;
+	do_count(n, 0);
+	if (runcount >= 1)
+		fatal("run operator used in invalid context", "");
+}

sys/src/cmd/spin/pangen2.h

@@ -34,18 +34,22 @@ static char *Pre0[] = {
 	"#include <string.h>",
 	"#include <ctype.h>",
 	"#include <errno.h>",
-"#ifdef SC",
+	"#if defined(WIN32) || defined(WIN64)",
+		"#include <time.h>",
+	"#else",
+		"#include <unistd.h>",
+		"#include <sys/times.h>",	/* new 4.3.0 */
+	"#endif",
 	"#include <sys/types.h>",	/* defines off_t */
 	"#include <sys/stat.h>",
 	"#include <fcntl.h>",
-	#ifndef PC
-	"#include <unistd.h>",
-	#endif
-"#endif",
 	"#define Offsetof(X, Y)	((unsigned long)(&(((X *)0)->Y)))",
 	"#ifndef max",
 	"#define max(a,b) (((a)<(b)) ? (b) : (a))",
 	"#endif",
+	"#ifndef PRINTF",
+	"int Printf(const char *fmt, ...); /* prototype only */",
+	"#endif",
 	0,
 };
 
@@ -89,13 +93,12 @@ static char *Preamble[] = {
 	"	}",
 	"#endif",
 "#endif",
-
 	"struct H_el {",
 	"	struct H_el *nxt;",
 	"#ifdef FULLSTACK",
-	"	unsigned tagged;",
+	"	unsigned int tagged;",
 		"#if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)",
-		"	unsigned proviso;", /* uses just 1 bit 0/1 */
+		"	unsigned int proviso;", /* uses just 1 bit 0/1 */
 		"#endif",
 	"#endif",
 	"#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))",
@@ -108,8 +111,8 @@ static char *Preamble[] = {
 	"	unsigned long ln;",	/* length of vector */
 		"#endif",
 	"#endif",
-	"#ifdef REACH",
-	"	unsigned D;",
+	"#if !defined(SAFETY) || defined(REACH)",
+	"	unsigned int D;",
 	"#endif",
 	"	unsigned state;",
 	"} **H_tab, **S_Tab;\n",
@@ -233,7 +236,7 @@ static char *Preamble[] = {
 	"long	Ccheck=0, Cholds=0;",
 	"int	a_cycles=0, upto=1, strict=0, verbose = 0, signoff = 0;",
 	"#ifdef HAS_CODE",
-	"int	gui = 0, coltrace = 0, readtrail = 0, whichtrail = 0, onlyproc = -1;",
+	"int	gui = 0, coltrace = 0, readtrail = 0, whichtrail = 0, onlyproc = -1, silent = 0;",
 	"#endif",
 	"int	state_tables=0, fairness=0, no_rck=0, Nr_Trails=0;",
 	"char	simvals[128];",
@@ -283,7 +286,8 @@ static char *Preamble[] = {
 	"static long udmem;",
 #endif
 	"#endif",
-	"static long	A_depth = 0, depth = 0;",
+	"static long	A_depth = 0;",
+	"long	depth = 0;",	/* not static to support -S2 option, but possible clash with embedded code */
 	"static uchar	warned = 0, iterative = 0, like_java = 0, every_error = 0;",
 	"static uchar	noasserts = 0, noends = 0, bounded = 0;",
 	"#if SYNC>0 && ASYNC==0",
@@ -677,16 +681,16 @@ static char *Tail[] = {
 	"	for (i = 1; i < m; i++)",
 	"	{	int nrelse;",
 	"		if (strcmp(procname[n], \":never:\") != 0)",
-	"		for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
-	"		{	if (T0->st == i",
-	"			&& strcmp(T0->tp, \"(1)\") == 0)",
-	"			{	printf(\"error: proctype '%%s' \",",
-	"					procname[n]);",
-	"		  		printf(\"line %%d, state %%d: has un\",",
-	"					srcln[i], i);",
-	"				printf(\"conditional self-loop\\n\");",
-	"				pan_exit(1);",
-	"		}	}",
+	"		{	for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
+	"			{	if (T0->st == i",
+	"				&& strcmp(T0->tp, \"(1)\") == 0)",
+	"				{	printf(\"error: proctype '%%s' \",",
+	"						procname[n]);",
+	"		  			printf(\"line %%d, state %%d: has un\",",
+	"						srcln[i], i);",
+	"					printf(\"conditional self-loop\\n\");",
+	"					pan_exit(1);",
+	"		}	}	}",
 	"		nrelse = 0;",
 	"		for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 	"		{	if (strcmp(T0->tp, \"else\") == 0)",
@@ -699,6 +703,17 @@ static char *Tail[] = {
 	"		  	printf(\" 'else' stmnts\\n\");",
 	"			pan_exit(1);",
 	"	}	}",
+	"	if (!state_tables && strcmp(procname[n], \":never:\") == 0)",
+	"	{	int h = 0;",
+	"		for (i = 1; i < m; i++)",
+	"		for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
+	"			if (T0->forw > h) h = T0->forw;",
+	"		h++;",
+	"		frm_st0 = (short *) emalloc(h * sizeof(short));",
+	"		for (i = 1; i < m; i++)",
+	"		for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
+	"			frm_st0[T0->forw] = i;",
+	"	}",
 	"}",
 	"void",
 	"imed(Trans *T, int v, int n, int j)	/* set intermediate state */",

sys/src/cmd/spin/pangen3.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern FILE	*th;
 extern int	claimnr, eventmapnr;
@@ -62,7 +58,8 @@ putfnm(int j, Symbol *s)
 static void
 putfnm_flush(int j)
 {
-	fprintf(th, "{ %s, %d, %d }\n",
+	if (lastfnm)
+		fprintf(th, "{ %s, %d, %d }\n",
 			lastfnm->name,
 			lastfrom, j);
 }

sys/src/cmd/spin/pangen3.h

@@ -37,8 +37,8 @@ static char *Head0[] = {
 	"	int back;	/* index return  transition */",
 	"	struct Trans *nxt;",
 	"} Trans;\n",
-	"#define qptr(x)	(((uchar *)&now)+q_offset[x])",
-	"#define pptr(x)	(((uchar *)&now)+proc_offset[x])",
+	"#define qptr(x)	(((uchar *)&now)+(int)q_offset[x])",
+	"#define pptr(x)	(((uchar *)&now)+(int)proc_offset[x])",
 /*	"#define Pptr(x)	((proc_offset[x])?pptr(x):noptr)",	*/
 	"extern uchar *Pptr(int);",
 
@@ -72,7 +72,7 @@ static char *Header[] = {
 		"#endif",
 	"#else",
 		"#ifdef BITSTATE",
-			"#ifdef SAFETY",
+			"#ifdef SAFETY && !defined(HASH64)",
 				"#define CNTRSTACK",
 			"#else",
 				"#define FULLSTACK",
@@ -163,13 +163,16 @@ static char *Header0[] = {
 	"struct H_el *Lstate;",
 	"#endif",
 	"int depthfound = -1;	/* loop detection */",
-	"int proc_offset[MAXPROC], proc_skip[MAXPROC];",
-	"int q_offset[MAXQ], q_skip[MAXQ];",
-	"#if VECTORSZ<65536",
-	"	unsigned short vsize;",
+	"#if VECTORSZ>32000",
+	"int proc_offset[MAXPROC];",
+	"int q_offset[MAXQ];",
 	"#else",
-	"	unsigned long  vsize;	/* vector size in bytes */",
+	"short proc_offset[MAXPROC];",
+	"short q_offset[MAXQ];",
 	"#endif",
+	"uchar proc_skip[MAXPROC];",
+	"uchar q_skip[MAXQ];",
+	"unsigned long  vsize;	/* vector size in bytes */",
 	"#ifdef SVDUMP",
 	"int vprefix=0, svfd;		/* runtime option -pN */",
 	"#endif",
@@ -251,10 +254,10 @@ static char *Addp1[] = {
 	"	else",
 	"		proc_skip[h] = 0;",
 	"#ifndef NOCOMP",
-	"	for (k = vsize + proc_skip[h]; k > vsize; k--)",
+	"	for (k = vsize + (int) proc_skip[h]; k > vsize; k--)",
 	"		Mask[k-1] = 1; /* align */",
 	"#endif",
-	"	vsize += proc_skip[h];",
+	"	vsize += (int) proc_skip[h];",
 	"	proc_offset[h] = vsize;",
 	"#ifdef SVDUMP",
 	"	if (vprefix > 0)",
@@ -262,7 +265,11 @@ static char *Addp1[] = {
 	"		write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */",
 	"		write(svfd, (uchar *) &h, sizeof(int));",
 	"		write(svfd, (uchar *) &n, sizeof(int));",
+	"#if VECTORSZ>32000",
 	"		write(svfd, (uchar *) &proc_offset[h], sizeof(int));",
+	"#else",
+	"		write(svfd, (uchar *) &proc_offset[h], sizeof(short));",
+	"#endif",
 	"		write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */",
 	"	}",
 	"#endif",
@@ -326,10 +333,10 @@ static char *Addq1[] = {
 	"#ifndef BFS",
 	"	if (is_rv) k += j;",
 	"#endif",
-	"	for (k += q_skip[i]; k > vsize; k--)",
+	"	for (k += (int) q_skip[i]; k > vsize; k--)",
 	"		Mask[k-1] = 1;",
 	"#endif",
-	"	vsize += q_skip[i];",
+	"	vsize += (int) q_skip[i];",
 	"	q_offset[i] = vsize;",
 	"	now._nr_qs += 1;",
 	"	vsize += j;",
@@ -536,7 +543,7 @@ static char *Code0[] = {
 	"run(void)",
 	"{	/* int i; */",
 	"	memset((char *)&now, 0, sizeof(State));",
-	"	vsize = sizeof(State) - VECTORSZ;",
+	"	vsize = (unsigned long) (sizeof(State) - VECTORSZ);",
 	"#ifndef NOVSZ",
 	"	now._vsz = vsize;",
 	"#endif",
@@ -736,14 +743,16 @@ static char *Proto[] = {
 	"char *emalloc(unsigned long);",
 	"char *Malloc(unsigned long);",
 	"int Boundcheck(int, int, int, int, Trans *);",
-	"/* int abort(void); */",
 	"int addqueue(int, int);",
 	"/* int atoi(char *); */",
-	"int close(int);",
-"#ifndef SC",
+	"/* int abort(void); */",
+	"int close(int);",	/* should probably remove this */
+#if 0
+	"#ifndef SC",
 	"int creat(char *, unsigned short);",
 	"int write(int, void *, unsigned);",
-"#endif",
+	"#endif",
+#endif
 	"int delproc(int, int);",
 	"int endstate(void);",
 	"int hstore(char *, int);",

sys/src/cmd/spin/pangen4.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern FILE	*tc, *tb;
 extern Queue	*qtab;

sys/src/cmd/spin/pangen4.h

@@ -27,7 +27,7 @@ static char *Dfa[] = {
 	"#define ushort	unsigned short",
 	"",
 	"#define TWIDTH		256",
-	"#define HASH(y,n)	(n)*(((int)y))",
+	"#define HASH(y,n)	(n)*(((long)y))",
 	"#define INRANGE(e,h)	((h>=e->From && h<=e->To)||(e->s==1 && e->S==h))",
 	"",
 	"extern char	*emalloc(unsigned long);	/* imported routine  */",

sys/src/cmd/spin/pangen5.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 typedef struct BuildStack {
 	FSM_trans *t;

sys/src/cmd/spin/pangen6.c

@@ -17,11 +17,7 @@
 /*      AST_criteria to process the slice criteria          */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern Ordered	 *all_names;
 extern FSM_use   *use_free;
@@ -507,8 +503,7 @@ AST_mutual(Lextok *a, Lextok *b, int toplevel)
 	if (strcmp(as->name, bs->name) != 0)
 		return 0;
 
-	if (as->type == STRUCT
-	&&  a && a->rgt && b && b->rgt)
+	if (as->type == STRUCT && a->rgt && b->rgt)
 		return AST_mutual(a->rgt->lft, b->rgt->lft, 0);
 
 	return 1;
@@ -2195,7 +2190,7 @@ init_dom(AST *a)
 				f->dom[i] = (ulong) ~0;			/* all 1's */
 
 			if (a->nstates % BPW)
-			for (i = a->nstates % BPW; i < BPW; i++)
+			for (i = (a->nstates % BPW); i < (int) BPW; i++)
 				f->dom[a->nwords-1] &= ~(1<<i);	/* clear tail */
 
 			for (cnt = 0; cnt < a->nstates; cnt++)

sys/src/cmd/spin/pc_zpp.c

@@ -376,9 +376,9 @@ static struct Directives {
 	{ 6, "define",	 do_define,	1 },
 	{ 4, "else",	 do_else,	0 },
 	{ 5, "endif",	 do_endif,	0 },
-	{ 2, "if",	 do_if,		0 },
 	{ 5, "ifdef",	 do_ifdef,	0 },
 	{ 6, "ifndef",   do_ifndef,	0 },
+	{ 2, "if",	 do_if,		0 },
 	{ 7, "include",  do_include,	1 },
 	{ 8, "undefine", do_undefine,	1 },
 };
@@ -390,7 +390,7 @@ process(char *q, int lno, char *fnm)
 	for (p = q; *p; p++)
 		if (*p != ' ' && *p != '\t')
 			break;
-	for (i = 0; i < sizeof(s)/sizeof(struct Directives); i++)
+	for (i = 0; i < (int) (sizeof(s)/sizeof(struct Directives)); i++)
 		if (!strncmp(s[i].directive, p, s[i].len))
 		{	if (s[i].interp
 			&&  !printing[if_depth])

sys/src/cmd/spin/reprosrc.c

@@ -11,11 +11,7 @@
 
 #include <stdio.h>
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 static int indent = 1;
 

sys/src/cmd/spin/run.c

@@ -11,11 +11,7 @@
 
 #include <stdlib.h>
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern RunList	*X, *run;
 extern Symbol	*Fname;
@@ -441,9 +437,9 @@ int
 interprint(FILE *fd, Lextok *n)
 {	Lextok *tmp = n->lft;
 	char c, *s = n->sym->name;
-	int i, j; char lbuf[16];
+	int i, j; char lbuf[512];
 	extern char Buf[];
-	char tBuf[1024];
+	char tBuf[4096];
 
 	Buf[0] = '\0';
 	if (!no_print)
@@ -494,7 +490,7 @@ append:			 strcat(Buf, lbuf);
 		}
 		dotag(fd, Buf);
 	}
-	if (strlen(Buf) > 1024) fatal("printf string too long", 0);
+	if (strlen(Buf) > 4096) fatal("printf string too long", 0);
 	return 1;
 }
 

sys/src/cmd/spin/sched.c

@@ -11,11 +11,7 @@
 
 #include <stdlib.h>
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern int	verbose, s_trail, analyze, no_wrapup;
 extern char	*claimproc, *eventmap, Buf[];
@@ -181,6 +177,31 @@ enable(Lextok *m)
 	return 0; /* process not found */
 }
 
+void
+check_param_count(int i, Lextok *m)
+{	ProcList *p;
+	Symbol *s = m->sym;	/* proctype name */
+	Lextok *f, *t;		/* formal pars */
+	int cnt = 0;
+
+	for (p = rdy; p; p = p->nxt)
+	{	if (strcmp(s->name, p->n->name) == 0)
+		{	if (m->lft)	/* actual param list */
+			{	lineno = m->lft->ln;
+				Fname  = m->lft->fn;
+			}
+			for (f = p->p;   f; f = f->rgt) /* one type at a time */
+			for (t = f->lft; t; t = t->rgt)	/* count formal params */
+			{	cnt++;
+			}
+			if (i != cnt)
+			{	printf("spin: saw %d parameters, expected %d\n", i, cnt);
+				non_fatal("wrong number of parameters", "");
+			}
+			break;
+	}	}
+}
+
 void
 start_claim(int n)
 {	ProcList *p;
@@ -291,6 +312,7 @@ static Element *
 silent_moves(Element *e)
 {	Element *f;
 
+	if (e->n)
 	switch (e->n->ntyp) {
 	case GOTO:
 		if (Rvous) break;
@@ -310,29 +332,33 @@ silent_moves(Element *e)
 	return e;
 }
 
-static void
-pickproc(void)
+static RunList *
+pickproc(RunList *Y)
 {	SeqList *z; Element *has_else;
 	short Choices[256];
 	int j, k, nr_else = 0;
 
 	if (nproc <= nstop+1)
 	{	X = run;
-		return;
+		return NULL;
 	}
 	if (!interactive || depth < jumpsteps)
 	{	/* was: j = (int) Rand()%(nproc-nstop); */
 		if (Priority_Sum < nproc-nstop)
 			fatal("cannot happen - weights", (char *)0);
 		j = (int) Rand()%Priority_Sum;
+
 		while (j - X->priority >= 0)
 		{	j -= X->priority;
+			Y = X;
 			X = X->nxt;
-			if (!X) X = run;
+			if (!X) { Y = NULL; X = run; }
 		}
 	} else
 	{	int only_choice = -1;
 		int no_choice = 0, proc_no_ch, proc_k;
+
+		Tval = 0;	/* new 4.2.6 */
 try_again:	printf("Select a statement\n");
 try_more:	for (X = run, k = 1; X; X = X->nxt)
 		{	if (X->pid > 255) break;
@@ -444,7 +470,8 @@ try_more:	for (X = run, k = 1; X; X = X->nxt)
 				goto try_again;
 		}	}
 		MadeChoice = 0;
-		for (X = run; X; X = X->nxt)
+		Y = NULL;
+		for (X = run; X; Y = X, X = X->nxt)
 		{	if (!X->nxt
 			||   X->nxt->pid > 255
 			||   j < Choices[X->nxt->pid])
@@ -453,12 +480,13 @@ try_more:	for (X = run, k = 1; X; X = X->nxt)
 				break;
 		}	}
 	}
+	return Y;
 }
 
 void
 sched(void)
 {	Element *e;
-	RunList *Y=0;	/* previous process in run queue */
+	RunList *Y = NULL;	/* previous process in run queue */
 	RunList *oX;
 	int go, notbeyond = 0;
 #ifdef PC
@@ -489,7 +517,7 @@ sched(void)
 	printf("warning: trace assertion not used in random simulation\n");
 
 	X = run;
-	pickproc();
+	Y = pickproc(Y);
 
 	while (X)
 	{	context = X->n;
@@ -564,7 +592,7 @@ sched(void)
 
 			if (X->pc->n->ntyp == '@'
 			&&  X->pid == (nproc-nstop-1))
-			{	if (X != run)
+			{	if (X != run && Y != NULL)
 					Y->nxt = X->nxt;
 				else
 					run = X->nxt;
@@ -578,6 +606,8 @@ sched(void)
 				if (!interactive) Tval = 0;
 				if (nproc == nstop) break;
 				memset(is_blocked, 0, 256);
+				/* proc X is no longer in runlist */
+				X = (X->nxt) ? X->nxt : run;
 			} else
 			{	if (p_blocked(X->pid))
 				{	if (Tval) break;
@@ -588,8 +618,7 @@ sched(void)
 						dotag(stdout, "timeout\n");
 						X = oX;
 		}	}	}	}
-		Y = X;
-		pickproc();
+		Y = pickproc(X);
 		notbeyond = 0;
 	}
 	context = ZS;

sys/src/cmd/spin/spin.h

@@ -15,8 +15,6 @@
 #include <stdio.h>
 #include <string.h>
 #include <ctype.h>
-#ifndef PC
-#endif
 
 typedef struct Lextok {
 	unsigned short	ntyp;	/* node type */
@@ -53,7 +51,7 @@ typedef struct Symbol {
 				   1=hide, 2=show,
 				   4=bit-equiv,   8=byte-equiv,
 				  16=formal par, 32=inline par,
-				  64=treat as if local
+				  64=treat as if local; 128=read at least once
 				 */
 	unsigned char	colnr;	/* for use with xspin during simulation */
 	int	nbits;		/* optional width specifier */
@@ -319,6 +317,7 @@ void	c_track(Symbol *, Symbol *, Symbol *);
 void	c_var(FILE *, char *, Symbol *);
 void	c_wrapper(FILE *);
 void	chanaccess(void);
+void	check_param_count(int, Lextok *);
 void	checkrun(Symbol *, int);
 void	comment(FILE *, Lextok *, int);
 void	cross_dsteps(Lextok *, Lextok *);

sys/src/cmd/spin/spin.y

@@ -21,6 +21,8 @@ extern  int	u_sync, u_async, dumptab;
 extern	short	has_sorted, has_random, has_enabled, has_pcvalue, has_np;
 extern	short	has_code, has_state, has_io;
 extern	void	count_runs(Lextok *);
+extern	void	no_internals(Lextok *);
+extern	void	any_runs(Lextok *);
 extern	void	validref(Lextok *, Lextok *);
 extern	char	yytext[];
 
@@ -375,7 +377,7 @@ sfld	: /* empty */		{ $$ = ZN; }
 stmnt	: Special		{ $$ = $1; }
 	| Stmnt			{ $$ = $1;
 				  if (inEventMap)
-				   fatal("not an event", (char *)0);
+				   non_fatal("not an event", (char *)0);
 				}
 	;
 
@@ -388,6 +390,7 @@ Special : varref RCV		{ Expand_Ok++; }
 	  margs			{ Expand_Ok--; has_io++;
 				  $$ = nn($1, 's', $1, $4);
 				  $$->val=0; trackchanuse($4, ZN, 'S');
+				  any_runs($4);
 				}
 	| IF options FI 	{ $$ = nn($1, IF, ZN, ZN);
         			  $$->sl = $2->sl;
@@ -422,11 +425,13 @@ Special : varref RCV		{ Expand_Ok++; }
 Stmnt	: varref ASGN expr	{ $$ = nn($1, ASGN, $1, $3);
 				  trackvar($1, $3);
 				  nochan_manip($1, $3, 0);
+				  no_internals($1);
 				}
 	| varref INCR		{ $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
 				  $$ = nn(ZN,  '+', $1, $$);
 				  $$ = nn($1, ASGN, $1, $$);
 				  trackvar($1, $1);
+				  no_internals($1);
 				  if ($1->sym->type == CHAN)
 				   fatal("arithmetic on chan", (char *)0);
 				}
@@ -434,6 +439,7 @@ Stmnt	: varref ASGN expr	{ $$ = nn($1, ASGN, $1, $3);
 				  $$ = nn(ZN,  '-', $1, $$);
 				  $$ = nn($1, ASGN, $1, $$);
 				  trackvar($1, $1);
+				  no_internals($1);
 				  if ($1->sym->type == CHAN)
 				   fatal("arithmetic on chan id's", (char *)0);
 				}
@@ -466,6 +472,7 @@ Stmnt	: varref ASGN expr	{ $$ = nn($1, ASGN, $1, $3);
 				  $$ = nn($1, 's', $1, $4);
 				  $$->val = has_sorted = 1;
 				  trackchanuse($4, ZN, 'S');
+				  any_runs($4);
 				}
 	| full_expr		{ $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
 	| ELSE  		{ $$ = nn(ZN,ELSE,ZN,ZN);

sys/src/cmd/spin/spinlex.c

@@ -11,11 +11,7 @@
 
 #include <stdlib.h>
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 #define MAXINL	16	/* max recursion depth inline fcts */
 #define MAXPAR	32	/* max params to an inline call */
@@ -542,7 +538,7 @@ c_add_stack(FILE *fd)
 		cnt++;
 	}
 
-	if (cnt == 0) fprintf(fd, "4"); /* can't happen */
+	if (cnt == 0) fprintf(fd, "WS"); /* can't happen */
 	fprintf(fd, "];\n");
 }
 
@@ -614,7 +610,7 @@ c_add_def(FILE *fd)	/* 3 - called in plunk_c_fcts() */
 	}
 
 	if (has_stack)
-	{	fprintf(fd, "void\nc_stack(char *p_t_r)\n{\n");
+	{	fprintf(fd, "void\nc_stack(uchar *p_t_r)\n{\n");
 		fprintf(fd, "#ifdef VERBOSE\n");
 		fprintf(fd, "	printf(\"c_stack %%u\\n\", p_t_r);\n");
 		fprintf(fd, "#endif\n");
@@ -632,7 +628,7 @@ c_add_def(FILE *fd)	/* 3 - called in plunk_c_fcts() */
 		fprintf(fd, "}\n\n");
 	}
 
-	fprintf(fd, "void\nc_update(char *p_t_r)\n{\n");
+	fprintf(fd, "void\nc_update(uchar *p_t_r)\n{\n");
 	fprintf(fd, "#ifdef VERBOSE\n");
 	fprintf(fd, "	printf(\"c_update %%u\\n\", p_t_r);\n");
 	fprintf(fd, "#endif\n");
@@ -662,7 +658,7 @@ c_add_def(FILE *fd)	/* 3 - called in plunk_c_fcts() */
 	fprintf(fd, "}\n");
 
 	if (has_stack)
-	{	fprintf(fd, "void\nc_unstack(char *p_t_r)\n{\n");
+	{	fprintf(fd, "void\nc_unstack(uchar *p_t_r)\n{\n");
 		fprintf(fd, "#ifdef VERBOSE\n");
 		fprintf(fd, "	printf(\"c_unstack %%u\\n\", p_t_r);\n");
 		fprintf(fd, "#endif\n");
@@ -677,7 +673,7 @@ c_add_def(FILE *fd)	/* 3 - called in plunk_c_fcts() */
 		fprintf(fd, "}\n");
 	}
 
-	fprintf(fd, "void\nc_revert(char *p_t_r)\n{\n");
+	fprintf(fd, "void\nc_revert(uchar *p_t_r)\n{\n");
 	fprintf(fd, "#ifdef VERBOSE\n");
 	fprintf(fd, "	printf(\"c_revert %%u\\n\", p_t_r);\n");
 	fprintf(fd, "#endif\n");
@@ -1358,7 +1354,29 @@ yylex(void)
 		{	sprintf(yytext, "'%c'", yylval->val);
 			strcat(IArg_cont[IArgno], yytext);
 		} else
-		{	strcat(IArg_cont[IArgno], yytext);
+		{
+			switch (c) {
+			case SEP:	strcpy(yytext, "::"); break;
+			case SEMI:	strcpy(yytext, ";"); break;
+			case DECR:	strcpy(yytext, "--"); break;
+			case INCR: 	strcpy(yytext, "++"); break;
+			case LSHIFT:	strcpy(yytext, "<<"); break;
+			case RSHIFT:	strcpy(yytext, ">>"); break;
+			case LE:	strcpy(yytext, "<="); break;
+			case LT:	strcpy(yytext, "<"); break;
+			case GE:	strcpy(yytext, ">="); break;
+			case GT:	strcpy(yytext, ">"); break;
+			case EQ:	strcpy(yytext, "=="); break;
+			case ASGN:	strcpy(yytext, "="); break;
+			case NE:	strcpy(yytext, "!="); break;
+			case R_RCV:	strcpy(yytext, "??"); break;
+			case RCV:	strcpy(yytext, "?"); break;
+			case O_SND:	strcpy(yytext, "!!"); break;
+			case SND:	strcpy(yytext, "!"); break;
+			case AND: 	strcpy(yytext, "&&"); break;
+			case OR:	strcpy(yytext, "||"); break;
+			}
+			strcat(IArg_cont[IArgno], yytext);
 		}
 	}
 

sys/src/cmd/spin/structs.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 typedef struct UType {
 	Symbol *nm;	/* name of the type */

sys/src/cmd/spin/sym.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern Symbol	*Fname, *owner;
 extern int	lineno, depth, verbose, NamesNotAdded, deadvar;
@@ -179,6 +175,7 @@ trackchanuse(Lextok *m, Lextok *w, int t)
 void
 setptype(Lextok *n, int t, Lextok *vis)	/* predefined types */
 {	int oln = lineno, cnt = 1; extern int Expand_Ok;
+
 	while (n)
 	{	if (n->sym->type && !(n->sym->hidden&32))
 		{ lineno = n->ln; Fname = n->fn;
@@ -193,7 +190,7 @@ setptype(Lextok *n, int t, Lextok *vis)	/* predefined types */
 			setaccess(n->sym, ZS, cnt, 'F');
 		}
 		if (t == UNSIGNED)
-		{	if (n->sym->nbits < 0)
+		{	if (n->sym->nbits < 0 || n->sym->nbits >= 32)
 			fatal("(%s) has invalid width-field", n->sym->name);
 			if (n->sym->nbits == 0)
 			{	n->sym->nbits = 16;
@@ -275,7 +272,7 @@ setxus(Lextok *p, int t)
 	if (!context)
 	{	lineno = p->ln;
 		Fname = p->fn;
-		non_fatal("non-local x[rs] assertion", (char *)0);
+		fatal("non-local x[rs] assertion", (char *)0);
 	}
 	for (m = p; m; m = m->rgt)
 	{	Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok));
@@ -325,7 +322,7 @@ setmtype(Lextok *m)
 
 		/* label the name */
 		if (n->lft->sym->type != MTYPE)
-		{	n->lft->sym->hidden |= 32;
+		{	n->lft->sym->hidden |= 128;	/* is used */
 			n->lft->sym->type = MTYPE;
 			n->lft->sym->ini = nn(ZN,CONST,ZN,ZN);
 			n->lft->sym->ini->val = cnt;
@@ -477,7 +474,7 @@ chan_check(Symbol *sp)
 		return;
 report:
 	chname(sp);
-	for (i = d = 0; i < sizeof(xx)/sizeof(struct X); i++)
+	for (i = d = 0; i < (int) (sizeof(xx)/sizeof(struct X)); i++)
 	{	b = 0;
 		for (a = sp->access; a; a = a->lnk)
 			if (a->typ == xx[i].typ) b++;
@@ -513,7 +510,7 @@ chanaccess(void)
 		case SHORT:
 		case INT:
 		case UNSIGNED:
-			if ((walk->entry->hidden&32))
+			if ((walk->entry->hidden&128))	/* was: 32 */
 				continue;
 
 			if (!separate

sys/src/cmd/spin/tl_lex.c

@@ -28,7 +28,7 @@ static void
 tl_getword(int first, int (*tst)(int))
 {	int i=0; char c;
 
-	yytext[i++]= (char ) first;
+	yytext[i++] = (char ) first;
 	while (tst(c = tl_Getchar()))
 		yytext[i++] = c;
 	yytext[i] = '\0';

sys/src/cmd/spin/tl_main.c

@@ -38,6 +38,23 @@ tl_Getchar(void)
 	return -1;
 }
 
+void
+tl_balanced(void)
+{	int i;
+	int k = 0;
+
+	for (i = 0; i < hasuform; i++)
+	{	if (uform[i] == '(')
+		{	k++;
+		} else if (uform[i] == ')')
+		{	k--;
+	}	}
+	if (k != 0)
+	{	tl_errs++;
+		tl_yyerror("parentheses not balanced");
+	}
+}
+
 void
 put_uform(void)
 {
@@ -96,7 +113,11 @@ nogood:		printf("usage:\tspin [-v] [-n] -f formula\n");
 		printf("	-n normalize tl formula and exit\n");
 		exit(1);
 	}
-	tl_parse();
+	tl_balanced();
+
+	if (tl_errs == 0)
+		tl_parse();
+
 	if (tl_verbose) tl_stats();
 	return tl_errs;
 }

sys/src/cmd/spin/tl_parse.c

@@ -15,7 +15,7 @@
 #include "tl.h"
 
 extern int	tl_yylex(void);
-extern int	tl_verbose;
+extern int	tl_verbose, tl_errs;
 
 int	tl_yychar = 0;
 YYSTYPE	tl_yylval;
@@ -391,5 +391,10 @@ tl_parse(void)
 		dump(n);
 		printf("\n");
 	}
+	if (tl_Getchar() != -1)
+	{	tl_yyerror("syntax error");
+		tl_errs++;
+		return;
+	}
 	trans(n);
 }

sys/src/cmd/spin/vars.c

@@ -10,11 +10,7 @@
 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
 
 #include "spin.h"
-#ifdef PC
-#include "y_tab.h"
-#else
 #include "y.tab.h"
-#endif
 
 extern Ordered	*all_names;
 extern RunList	*X, *LastX;
@@ -278,9 +274,13 @@ dumpglobals(void)
 void
 dumplocal(RunList *r)
 {	static Lextok *dummy = ZN;
-	Symbol *z, *s = r->symtab;
+	Symbol *z, *s;
 	int i;
 
+	if (!r) return;
+
+	s = r->symtab;
+
 	if (!dummy)
 		dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN);
 

sys/src/cmd/spin/version.h

@@ -1 +1 @@
-#define Version	"Spin Version 4.2.5 -- 2 April 2005"
+#define Version	"Spin Version 4.3.0 -- 22 June 2007"