[Termination tools] Re: scaling up SRSs

[H. Zantema]

Dear Claude,

Thanks for including the examples in the database that fast. One minor 
remark: could you rename z2.srs to z02.srs (and more general zi to z0i for
i = 1..9)? Now we have the strange alphabetic order z19, z2, z20,....

Below you may find a few more examples. The last two originate from liveness
problems; maybe you can call them ring_prot and waiting_line rather than
z followed by a number.

		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+

aba -> abba
bab -> baab

ab -> df
c -> ba
df -> c

abb -> c
c -> bda
d -> ba

Ab -> baBA
Ba -> abAB
Aa -> 
Bb -> 

aabab -> bababaaa
ab -> acb
cab -> caab

aa -> bba
bb -> cab
cc -> aac

apbc -> caqdbapbap
paqd -> daqdbapbap

liveness for ring protocol:
rr -> sr
rs -> sr
rn -> sr
rb -> usb
ru -> ur
su -> us
nu -> un
tru -> tcr
tsu -> tcr
tnu -> tcr
cu -> uc
cs -> sc
cr -> rc
cn -> nc
cn -> n

liveness for single waiting line:
tf -> tcn
nf -> fn
of -> fo
ns -> fs
os -> fs
cf -> fc
cn -> nc
co -> oc
co -> o