Example #4 (MESI):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.101 ) = True ;
rm e.41 (e.101 ) = <F24 (e.41 ) (e.101 )> ;
s.102 e.41 (e.101 ) = <F35 (e.41 ) (e.101 )> ;
}
* InputFormat: <F35 (e.105 ) (e.106 ) e.107 >
F35 {
() (e.106 ) e.107 = True ;
(rm e.105 ) (I e.106 ) e.107 = <F24 (e.105 ) (e.106 e.107 ) I > ;
(rm e.105 ) () I e.107 = <F24 (e.105 ) (e.107 ) I > ;
(wh2 ) (e.106 ) e.107 = True ;
(wh2 rm e.105 ) (I e.106 ) e.107 = <F24 (e.105 ) (e.106 e.107 ) I > ;
(wh2 rm e.105 ) () I e.107 = <F24 (e.105 ) (e.107 ) I > ;
(wh2 s.113 e.105 ) (I e.106 ) e.107 = <F35 (e.105 ) (e.106 ) e.107 I >
;
(wh2 s.113 e.105 ) () I e.107 = <F35 (e.105 ) () e.107 I > ;
(s.110 e.105 ) (I e.106 ) e.107 = <F35 (e.105 ) (e.106 ) e.107 I > ;
(s.110 e.105 ) () I e.107 = <F35 (e.105 ) () e.107 I > ;
}
* InputFormat: <F24 (e.105 ) (e.106 ) e.107 >
F24 {
() (e.106 ) e.107 = True ;
(rm e.105 ) (I e.106 ) e.107 = <F24 (e.105 ) (e.106 ) I e.107 > ;
(wh3 e.105 ) (e.106 ) e.107 = <F35 (e.105 ) (e.106 ) e.107 > ;
(s.108 e.105 ) (I e.106 ) e.107 = <F35 (e.105 ) (e.106 ) I e.107 > ;
}
****************************** The End ************************************
|
Example #5 (MOESI):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.101 ) = True ;
rm e.41 (e.101 ) = <F24 (e.41 ) (e.101 )> ;
s.102 e.41 (e.101 ) = <F35 (e.41 ) (e.101 )> ;
}
* InputFormat: <F81 (e.116 ) (e.117 ) e.118 >
F81 {
() (e.117 ) e.118 = True ;
(rm e.116 ) (I e.117 ) e.118 = <F81 (e.116 ) (e.117 ) I e.118 > ;
(wh3A e.116 ) (e.117 ) e.118 = <F35 (e.116 ) (I e.118 e.117 )> ;
(wh3B e.116 ) (e.117 ) e.118 = <F35 (e.116 ) (I e.118 e.117 )> ;
(s.119 e.116 ) (I e.117 ) e.118 = <F35 (e.116 ) (I I e.118 e.117 )> ;
}
* InputFormat: <F35 (e.105 ) (e.106 ) e.107 >
F35 {
() (e.106 ) e.107 = True ;
(rm e.105 ) (e.106 ) I e.107 = <F24 (e.105 ) (e.107 e.106 ) I > ;
(rm e.105 ) (I e.106 ) = <F24 (e.105 ) (e.106 ) I > ;
(wh2 ) (e.106 ) e.107 = True ;
(wh2 rm e.105 ) (e.106 ) I e.107 = <F81 (e.105 ) (e.107 e.106 )> ;
(wh2 rm e.105 ) (I e.106 ) = <F81 (e.105 ) (e.106 )> ;
(wh2 s.113 e.105 ) (e.106 ) I e.107 = <F35 (e.105 ) (I e.107 e.106 )>
;
(wh2 s.113 e.105 ) (I e.106 ) = <F35 (e.105 ) (I e.106 )> ;
(s.110 e.105 ) (e.106 ) I e.107 = <F35 (e.105 ) (I e.107 e.106 )> ;
(s.110 e.105 ) (I e.106 ) = <F35 (e.105 ) (I e.106 )> ;
}
* InputFormat: <F24 (e.105 ) (e.106 ) e.107 >
F24 {
() (e.106 ) e.107 = True ;
(rm e.105 ) (I e.106 ) e.107 = <F24 (e.105 ) (e.106 ) I e.107 > ;
(wh3A e.105 ) (e.106 ) e.107 = <F35 (e.105 ) (e.106 ) e.107 > ;
(s.108 e.105 ) (I e.106 ) e.107 = <F35 (e.105 ) (I e.107 e.106 )> ;
}
****************************** The End ************************************
|
Example #6 (The University of Illinois):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
e.41 (e.101 ) = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F122 (e.106 ) (e.107 ) e.108 >
F122 {
() (e.107 ) e.108 = True ;
(r2 e.106 ) (e.107 ) = <F12 (e.106 ) I e.107 > ;
(r4A e.106 ) (e.107 ) I e.108 = <F34 (e.106 ) (I e.107 ) e.108 > ;
(r7 e.106 ) (e.107 ) I e.108 = <F102 (e.106 ) (e.107 e.108 )> ;
(r8 ) (e.107 ) e.108 = True ;
(r8 r3 e.106 ) (e.107 ) I e.108 = <F34 (e.106 ) (e.108 I e.107 )> ;
(r8 r3 e.106 ) (e.107 ) = <F34 (e.106 ) (e.107 )> ;
(r8 r8 e.106 ) (e.107 ) I e.108 = <F102 (e.106 ) (e.108 I e.107 )> ;
(r8 r8 e.106 ) (e.107 ) = <F102 (e.106 ) (e.107 )> ;
(r8 s.132 e.106 ) (e.107 ) e.108 = <F5 (e.106 ) e.108 I e.107 > ;
(s.128 e.106 ) (e.107 ) I e.108 = <F122 (e.106 ) (I e.107 ) e.108 > ;
}
* InputFormat: <F102 (e.106 ) (e.107 ) e.108 >
F102 {
() (e.107 ) e.108 = True ;
(r3 e.106 ) (e.107 ) e.108 = <F34 (e.106 ) (e.107 e.108 )> ;
(r8 e.106 ) (e.107 ) e.108 = <F102 (e.106 ) (e.107 ) e.108 > ;
(s.123 e.106 ) (e.107 ) e.108 = <F5 (e.106 ) I e.107 e.108 > ;
}
* InputFormat: <F46 (e.106 ) (e.107 ) e.108 >
F46 {
() (e.107 ) e.108 = True ;
(r3 e.106 ) (I e.107 ) e.108 = <F34 (e.106 ) (e.107 I e.108 )> ;
(r3 e.106 ) () e.108 = <F34 (e.106 ) (e.108 )> ;
(r8 e.106 ) (I e.107 ) e.108 = <F46 (e.106 ) (I e.107 ) e.108 > ;
(r8 e.106 ) () e.108 = <F46 (e.106 ) () e.108 > ;
(s.111 e.106 ) (e.107 ) e.108 = <F5 (e.106 ) e.107 I e.108 > ;
}
* InputFormat: <F34 (e.106 ) (e.107 ) e.108 >
F34 {
() (e.107 ) e.108 = True ;
(r4A e.106 ) (I e.107 ) e.108 = <F34 (e.106 ) (e.107 ) I e.108 > ;
(r7 e.106 ) (e.107 ) e.108 = <F46 (e.106 ) (e.107 ) e.108 > ;
(r8 e.106 ) (I e.107 ) e.108 = <F102 (e.106 ) (e.107 ) e.108 > ;
(s.109 ) (e.107 ) e.108 = True ;
(s.109 r4A e.106 ) (e.107 ) e.108 = <F34 (e.106 ) (e.107 ) e.108 > ;
(s.109 r7 e.106 ) (e.107 ) e.108 = <F102 (e.106 ) (e.107 ) e.108 > ;
(s.109 r8 e.106 ) (e.107 ) e.108 = <F102 (e.106 ) (e.108 e.107 )> ;
(s.109 s.121 e.106 ) (e.107 ) e.108 = <F122 (e.106 ) (e.107 ) e.108 >
;
}
* InputFormat: <F12 (e.41 ) e.101 >
F12 {
() e.101 = True ;
(r4B e.41 ) I e.101 = <F34 (e.41 ) (e.101 )> ;
(r6 ) e.101 = True ;
(r6 r3 e.41 ) I e.101 = <F34 (e.41 ) (e.101 )> ;
(r6 r8 e.41 ) I e.101 = <F102 (e.41 ) (e.101 )> ;
(r6 s.139 e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
(r8 e.41 ) I e.101 = <F102 (e.41 ) (e.101 )> ;
(s.103 e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F5 (e.41 ) e.101 >
F5 {
() e.101 = True ;
(r2 e.41 ) e.101 = <F12 (e.41 ) e.101 > ;
(s.102 ) e.101 = True ;
(s.102 r3 e.41 ) I e.101 = <F34 (e.41 ) (e.101 )> ;
(s.102 r8 e.41 ) I e.101 = <F102 (e.41 ) (e.101 )> ;
(s.102 s.145 e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
}
****************************** The End ************************************
|
Example #7 (Berkley):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.101 ) = True ;
rm e.41 (e.101 ) = <F24 (e.41 ) (e.101 )> ;
s.102 (e.101 ) = True ;
s.102 rm e.41 (I e.101 ) = <F101 (e.41 ) (e.101 )> ;
s.102 s.140 e.41 (I e.101 ) = <F81 (e.41 ) I e.101 > ;
}
* InputFormat: <F101 (e.126 ) (e.127 ) e.128 >
F101 {
() (e.127 ) e.128 = True ;
(rm e.126 ) (I e.127 ) e.128 = <F101 (e.126 ) (e.127 ) I e.128 > ;
(wm e.126 ) (I e.127 ) e.128 = <F81 (e.126 ) I e.128 I e.127 > ;
(wh1A e.126 ) (e.127 ) e.128 = <F81 (e.126 ) I e.128 e.127 > ;
(s.129 e.126 ) (e.127 ) e.128 = <F81 (e.126 ) e.128 I e.127 > ;
}
* InputFormat: <F81 (e.121 ) e.122 >
F81 {
() e.122 = True ;
(rm e.121 ) I e.122 = <F101 (e.121 ) (e.122 )> ;
(s.123 e.121 ) I e.122 = <F81 (e.121 ) I e.122 > ;
}
* InputFormat: <F24 (e.105 ) (e.106 ) e.107 >
F24 {
() (e.106 ) e.107 = True ;
(rm e.105 ) (I e.106 ) e.107 = <F24 (e.105 ) (e.106 ) I e.107 > ;
(wm e.105 ) (I e.106 ) e.107 = <F81 (e.105 ) I e.107 e.106 > ;
(s.108 ) (e.106 ) e.107 = True ;
(s.108 rm e.105 ) (e.106 ) I e.107 = <F101 (e.105 ) (e.107 e.106 )> ;
(s.108 rm e.105 ) (I e.106 ) = <F101 (e.105 ) (e.106 )> ;
(s.108 wm e.105 ) (e.106 ) I e.107 = <F81 (e.105 ) I e.107 e.106 > ;
(s.108 s.135 e.105 ) (I e.106 ) = <F81 (e.105 ) I e.106 > ;
}
****************************** The End ************************************
|
Example #8 (DEC Firefly):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.101 ) = True ;
rm_1 (e.101 ) = True ;
rm_1 rm_3B e.41 (I e.101 ) = <F31 e.41 > ;
rm_1 wh_2 e.41 (e.101 ) = <F54 e.41 > ;
rm_1 s.103 e.41 (I e.101 ) = <F54 e.41 > ;
s.102 e.41 (e.101 ) = <F54 e.41 > ;
}
* InputFormat: <F54 e.41 >
F54 {
= True ;
rm_2 e.41 = <F31 e.41 > ;
s.114 e.41 = <F54 e.41 > ;
}
* InputFormat: <F41 e.106 >
F41 {
= True ;
rm_2 e.106 = <F31 e.106 > ;
s.111 e.106 = <F41 e.106 > ;
}
* InputFormat: <F31 e.106 >
F31 {
= True ;
rm_3A e.106 = <F31 e.106 > ;
s.109 e.106 = <F41 e.106 > ;
}
****************************** The End ************************************
|
Example #9 (IEEE Futurebus+):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
e.41 (e.101 ) = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F311 (e.105 ) e.106 >
F311 {
() e.106 = True ;
(r2 e.105 ) I e.106 = <F99 (e.105 ) (e.106 ) ()> ;
(wm1 ) I e.106 = True ;
(wm1 s.180 e.105 ) I e.106 = <F274 (e.105 ) (e.106 I )> ;
(wm3 e.105 ) e.106 = <F311 (e.105 ) e.106 > ;
(s.178 e.105 ) e.106 = <F274 (e.105 ) (e.106 )> ;
}
* InputFormat: <F274 (e.120 ) (e.121 ) e.122 >
F274 {
() (e.121 ) e.122 = True ;
(r2 e.120 ) (e.121 ) I e.122 = <F162 (e.120 ) (e.122 e.121 )> ;
(r2 e.120 ) (I e.121 ) = <F162 (e.120 ) (e.121 )> ;
(wm1 ) (e.121 ) I e.122 = True ;
(wm1 s.173 e.120 ) (e.121 ) I e.122 = <F274 (e.120 ) (I e.122 e.121 )>
;
(wm1 ) (I e.121 ) = True ;
(wm1 s.175 e.120 ) (I e.121 ) = <F274 (e.120 ) (I e.121 )> ;
(s.170 e.120 ) (e.121 ) e.122 = <F274 (e.120 ) (e.122 e.121 )> ;
}
* InputFormat: <F213 (e.120 ) (e.121 ) e.122 >
F213 {
() (e.121 ) e.122 = True ;
(r2 e.120 ) (I e.121 ) e.122 = <F162 (e.120 ) (e.121 I e.122 )> ;
(r2 e.120 ) () e.122 = <F162 (e.120 ) (e.122 )> ;
(wm1 ) (I e.121 ) e.122 = True ;
(wm1 s.159 e.120 ) (I e.121 ) e.122 = <F213 (e.120 ) (I e.121 ) e.122 > ;
(wm1 ) () e.122 = True ;
(wm1 s.161 e.120 ) () e.122 = <F213 (e.120 ) () e.122 > ;
(s.156 e.120 ) (e.121 ) e.122 = <F213 (e.120 ) (e.121 ) e.122 > ;
}
* InputFormat: <F162 (e.137 ) (e.138 ) e.139 >
F162 {
() (e.138 ) e.139 = True ;
(r2 e.137 ) (I e.138 ) e.139 = <F162 (e.137 ) (e.138 ) I e.139 > ;
(r3 e.137 ) (e.138 ) e.139 = <F77 (e.137 ) (e.138 ) I e.139 > ;
(wm1 e.137 ) (I e.138 ) e.139 = <F114 (e.137 ) (e.138 ) () e.139 > ;
(s.143 e.137 ) (e.138 ) e.139 = <F162 (e.137 ) (e.138 ) e.139 > ;
}
* InputFormat: <F119 (e.126 ) (e.127 ) (e.128 ) e.129 >
F119 {
() (e.127 ) (e.128 ) e.129 = True ;
(r2 e.126 ) (I e.127 ) (e.128 ) e.129 = <F162 (e.126 ) (e.127 I e.129 I e.128 )> ;
(r2 e.126 ) () (e.128 ) e.129 = <F162 (e.126 ) (e.129 I e.128 )> ;
(wm1 ) (I e.127 ) (e.128 ) e.129 = True ;
(wm1 s.149 e.126) (I e.127) (e.128) e.129 = <F119 (e.126) (I e.127) (e.128) e.129 > ;
(wm1 ) () (e.128 ) e.129 = True ;
(wm1 s.151 e.126 ) () (e.128 ) e.129 = <F119 (e.126 ) () (e.128 ) e.129 > ;
(s.134 e.126 ) (e.127 ) (e.128 ) e.129 = <F119 (e.126 ) (e.127 ) (e.128) e.129 > ;
}
* InputFormat: <F114 (e.126 ) (e.127 ) (e.128 ) e.129 >
F114 {
() (e.127 ) (e.128 ) e.129 = True ;
(s.133 e.126 ) (e.127 ) (e.128 ) e.129 = <F119 (e.126 ) (e.127 ) (e.128) e.129 > ;
}
* InputFormat: <F99 (e.126 ) (e.127 ) (e.128 ) e.129 >
F99 {
() (e.127 ) (e.128 ) e.129 = True ;
(r2 e.126 ) (I e.127 ) (e.128 ) e.129 = <F99 (e.126 ) (e.127 ) (I e.128 ) e.129 > ;
(r4 e.126 ) (e.127 ) (e.128 ) e.129 = <F77 (e.126 ) (e.127 ) e.128 I e.129 > ;
(wm1 e.126 ) (I e.127 ) (e.128 ) e.129 = <F114 (e.126 ) (e.127 ) (e.128) e.129 > ;
(s.130 e.126 ) (e.127 ) (e.128 ) e.129 = <F99 (e.126 ) (e.127 ) (e.128) e.129 > ;
}
* InputFormat: <F77 (e.120 ) (e.121 ) e.122 >
F77 {
() (e.121 ) e.122 = True ;
(r2 e.120 ) (I e.121 ) e.122 = <F99 (e.120 ) (e.121 ) () e.122 > ;
(wm1 ) (I e.121 ) e.122 = True ;
(wm1 s.155 e.120 ) (I e.121 ) e.122 = <F213 (e.120 ) (e.121 ) e.122 > ;
(wm3 e.120 ) (e.121 ) e.122 = <F77 (e.120 ) (e.121 ) e.122 > ;
(s.123 e.120 ) (e.121 ) e.122 = <F274 (e.120 ) (e.121 ) e.122 > ;
}
* InputFormat: <F26 (e.105 ) (e.106 ) e.107 >
F26 {
() (e.106 ) e.107 = True ;
(r2 e.105 ) (I e.106 ) e.107 = <F26 (e.105 ) (e.106 ) I e.107 > ;
(r5 e.105 ) (e.106 ) I e.107 = <F77 (e.105 ) (e.106 ) I e.107 > ;
(r6 e.105 ) (e.106 ) = <F311 (e.105 ) e.106 > ;
(wm1 ) (I e.106 ) e.107 = True ;
(wm1 s.184 e.105 ) (I e.106 ) e.107 = <F274 (e.105 ) (e.106 I e.107 )> ;
(s.108 e.105 ) (e.106 ) e.107 = <F26 (e.105 ) (e.106 ) e.107 > ;
}
* InputFormat: <F5 (e.41 ) e.101 >
F5 {
() e.101 = True ;
(r2 e.41 ) e.101 = <F26 (e.41 ) (e.101 )> ;
(wm1 ) e.101 = True ;
(wm1 s.187 e.41 ) e.101 = <F274 (e.41 ) (e.101 )> ;
(s.102 e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
}
****************************** The End ************************************
|
Example #10 (Xerox PARC Dragon):
(A)
An incorrect specification given by G. Delzanno in
[2].
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.101 ) = True ;
rm1 (e.101 ) = True ;
rm1 rm2D e.41 (I e.101 ) = True ;
rm1 wm2D e.41 (I e.101 ) = True ;
rm1 s.103 e.41 (e.101 ) , <F295 (e.41 ) (e.101 )>:s.249 (e.250 ) = s.249 e.250 ;
s.102 e.41 (e.101 ) , <F295 (e.41 ) (e.101 )>:s.254 (e.255 ) = s.254 e.255 ;
}
* InputFormat: <F455 (e.206 ) (e.207 ) (e.208 ) e.209 >
F455 {
() (e.207 ) (e.208 ) I e.209 = False3 (I I e.209 ) ;
() (e.207 ) (e.208 ) e.209 = False1 () ;
(rm2A e.206 ) (I e.207 ) (e.208 ) e.209 = True () ;
(rm2B e.206 ) (I e.207 ) (e.208 ) e.209 = True () ;
(rm2C e.206 ) (I e.207 ) (e.208 ) e.209 = True () ;
(wm2A e.206 ) (I e.207 ) (e.208 ) e.209
, <F455 (e.206 ) (e.207 ) (I e.208 ) e.209 >:s.266 (e.267 ) = s.266 (e.267 ) ;
(wm2B e.206 ) (I e.207 ) (e.208 ) e.209
, <F455 (e.206 ) (e.207 ) (I e.208 ) e.209 >:s.268 (e.269 ) = s.268 (e.269 ) ;
(wm2C e.206 ) (I e.207 ) (e.208 ) e.209
, <F455 (e.206 ) (e.207 ) (I e.208 ) e.209 >:s.270 (e.271 ) = s.270 (e.271 ) ;
(wh5A e.206 ) (e.207 ) (I e.208 ) e.209
, <F455 (e.206 ) (e.207 ) (I e.208 ) e.209 >:s.272 (e.273 ) = s.272 (e.273 ) ;
(s.210 e.206 ) (e.207 ) (e.208 ) e.209
, <F455 (e.206 ) (e.207 ) (e.208 ) e.209 >:s.274 (e.275 ) = s.274 (e.275 ) ;
}
* InputFormat: <F295 (e.169 ) (e.170 ) e.171 >
F295 {
() (e.170 ) I e.171 = False3 (I I e.171 ) ;
() (e.170 ) e.171 = True () ;
(rm2C e.169 ) (I e.170 ) e.171 = True () ;
(s.172 ) (I e.170 ) I e.171 = False3 (I I e.171 ) ;
(s.172 ) (I e.170 ) e.171 = False1 () ;
(s.172 rm2B e.169 ) (I I e.170 ) e.171 = True () ;
(s.172 rm2C e.169 ) (I I e.170 ) e.171 = True () ;
(s.172 wm2B e.169 ) (I I e.170 ) e.171
, <F455 (e.169 ) (e.170 ) () e.171 >:s.223 (e.224 ) = s.223 (e.224 ) ;
(s.172 wm2C e.169 ) (I I e.170 ) e.171
, <F455 (e.169 ) (e.170 ) () e.171 >:s.232 (e.233 ) = s.232 (e.233 ) ;
(s.172 s.198 e.169 ) (I e.170 ) e.171
, <F295 (e.169 ) (e.170 ) I e.171 >:s.276 (e.277 ) = s.276 (e.277 ) ;
}
****************************** The End ************************************
|
(B)
The correct specification given by G. Delzanno
[3].
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
e.41 (e.101 ) = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F441 (e.431 ) (e.432 ) e.433 >
F441 {
(rm1 e.431 ) (e.432 ) = <F13 (e.431 ) e.432 > ;
(rm2A e.431 ) (e.432 ) I e.433 = <F324 (e.431 ) (e.432 ) I e.433 > ;
(wm1 rm2C e.431 ) (I e.432 ) = <F414 (e.431 ) (e.432 ) (I ) I > ;
(wm1 wm2C e.431 ) (s.465 e.432 ) = <F414 (e.431 ) (e.432 ) (I ) s.465 > ;
(wm1 s.456 e.431 ) (e.432 ) = <F5 (e.431 ) e.432 > ;
(wm2A e.431 ) (e.432 ) s.453 e.433 = <F414 (e.431 ) (e.432 ) (s.453 e.433 ) I > ;
(s.452 e.431 ) (e.432 ) I e.433 = <F441 (e.431 ) (I e.432 ) e.433 > ;
}
* InputFormat: <F414 (e.431 ) (e.432 ) (e.433 ) s.434 >
F414 {
(rm2A e.431 ) (I e.432 ) (I e.433 ) s.434 = <F414 (e.431) (e.432) (I I e.433) s.434> ;
(rm2B e.431 ) (I e.432 ) (e.433 ) I = <F414 (e.431 ) (e.432 ) (I e.433 ) I > ;
(wm2A e.431 ) (s.442 e.432 ) (s.443 e.433 ) s.434
= <F414 (e.431 ) (e.432 ) (s.434 s.443 e.433 ) s.442 > ;
(wm2B e.431 ) (s.444 e.432 ) (e.433 ) s.434
= <F414 (e.431 ) (e.432 ) (s.434 e.433 ) s.444 > ;
(wh2 e.431 ) (e.432 ) (I e.433 ) s.434 = <F414 (e.431 ) (I e.432 ) (e.433 ) s.434 > ;
(s.435 e.431 ) (e.432 ) (e.433 ) s.434 = <F441 (e.431 ) (e.432 ) e.433 > ;
}
* InputFormat: <F324 (e.358 ) (e.359 ) s.360 e.361 >
F324 {
(rm2A e.358 ) (I e.359 ) s.360 e.361 = <F324 (e.358 ) (e.359 ) I s.360 e.361 > ;
(wm2A e.358 ) (s.369 e.359 ) s.360 e.361 = <F414 (e.358) (e.359) (I s.360 e.361) s.369> ;
(s.362 e.358 ) (e.359 ) s.360 e.361 = <F441 (e.358 ) (e.359 ) s.360 e.361 > ;
}
* InputFormat: <F13 (e.41 ) e.101 >
F13 {
(rm2D e.41 ) I e.101 = <F324 (e.41 ) (e.101 ) I > ;
(wm2D e.41 ) s.113 e.101 = <F414 (e.41 ) (e.101 ) (I ) s.113 > ;
(s.103 e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F5 (e.41 ) e.101 >
F5 {
(rm1 e.41 ) e.101 = <F13 (e.41 ) e.101 > ;
(s.102 rm2C e.41 ) I e.101 = <F414 (e.41 ) (e.101 ) (I ) I > ;
(s.102 wm2C e.41 ) s.498 e.101 = <F414 (e.41 ) (e.101 ) (I ) s.498 > ;
(s.102 s.489 e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
}
****************************** The End ************************************
|
Example #11 (Java Meta-Locking Algorithm):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
e.41 (e.101 ) = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F201 (e.107 ) (e.108 ) e.110 >
F201 {
(e.107 ) (e.108 ) = True ;
(e.107 ) (I e.108 ) get_slow e.110 = <F201 (I e.107 ) (e.108 ) e.110 > ;
(e.107 ) (e.108 ) put_slow e.110 = <F63 (e.107 ) (e.108 ) e.110 > ;
(e.107 ) (e.108 ) s.144 e.110 = <F201 (e.107 ) (e.108 ) e.110 > ;
}
* InputFormat: <F165 (e.107 ) e.110 >
F165 {
(e.107 ) = True ;
(e.107 ) get_slow e.110 = True ;
(e.107 ) request e.110 = <F74 (e.107 ) e.110 > ;
(e.107 ) s.136 e.110 = <F165 (e.107 ) e.110 > ;
}
* InputFormat: <F135 e.110 >
F135 {
= True ;
get_fast e.110 = <F126 () e.110 > ;
s.128 e.110 = <F135 e.110 > ;
}
* InputFormat: <F126 (e.107 ) e.110 >
F126 {
(e.107 ) = True ;
() put_fast e.110 = <F135 e.110 > ;
(e.107 ) get_slow e.110 = True ;
(I e.107 ) put_slow e.110 = True ;
(e.107 ) s.127 e.110 = <F126 (e.107 ) e.110 > ;
}
* InputFormat: <F74 (e.107 ) e.110 >
F74 {
(e.107 ) = True ;
(e.107 ) get_slow e.110 = True ;
(e.107 ) go e.110 = <F126 (e.107 ) e.110 > ;
(e.107 ) s.117 e.110 = <F74 (e.107 ) e.110 > ;
}
* InputFormat: <F63 (e.107 ) (e.108 ) e.110 >
F63 {
(e.107 ) (e.108 ) = True ;
(e.107 ) (I e.108 ) get_slow e.110 = <F63 (I e.107 ) (e.108 ) e.110 > ;
(e.107 ) (e.108 ) release e.110 = <F74 (e.107 ) e.110 > ;
(e.107 ) (e.108 ) s.115 e.110 = <F63 (e.107 ) (e.108 ) e.110 > ;
}
* InputFormat: <F51 (e.107 ) (e.108 ) e.110 >
F51 {
(e.107 ) (e.108 ) = True ;
(e.107 ) (I e.108 ) get_slow e.110 = <F51 (I e.107 ) (e.108 ) e.110 > ;
(e.107 ) (e.108 ) request e.110 = <F63 (e.107 ) (e.108 ) e.110 > ;
(e.107 ) (e.108 ) release e.110 = <F165 (e.107 ) e.110 > ;
(e.107 ) (e.108 ) s.113 e.110 = <F51 (e.107 ) (e.108 ) e.110 > ;
}
* InputFormat: <F36 s.106 (e.107 ) (e.108 ) e.110 >
F36 {
put_fast () (e.108 ) e.110 = <F5 (e.110 ) I e.108 > ;
get_slow (e.107 ) (I e.108 ) = True ;
get_slow (e.107 ) (I e.108 ) s.112 e.110 = <F36 s.112 (I e.107 ) (e.108 ) e.110 > ;
put_slow (I e.107 ) (e.108 ) e.110 = <F51 (e.107 ) (e.108 ) e.110 > ;
request (I e.107 ) (e.108 ) e.110 = <F201 (e.107 ) (e.108 ) e.110 > ;
s.106 (e.107 ) (e.108 ) = True ;
s.106 (e.107 ) (e.108 ) s.148 e.110 = <F36 s.148 (e.107 ) (e.108 ) e.110 > ;
}
* InputFormat: <F5 (e.41 ) e.101 >
F5 {
() e.101 = True ;
(get_fast ) I e.101 = True ;
(get_fast s.103 e.41 ) I e.101 = <F36 s.103 () (e.101 ) e.41 > ;
(s.102 e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
}
****************************** The End ************************************
|
Example #12 (Reader-Writer protocol):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
e.41 (e.101 ) = <F5 e.41 > ;
}
* InputFormat: <F312 (e.154 ) (e.155 ) (e.157 ) e.158 >
F312 {
() (e.155 ) (e.157 ) e.158 = True ;
(r2 e.154 ) (e.155 ) (I e.157 ) e.158 = <F312 (e.154 ) (I e.155 ) (e.157 ) e.158 > ;
(r4 e.154 ) (e.155 ) (e.157 ) e.158 = <F235 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(r5 e.154 ) (e.155 ) (e.157 ) e.158 = <F302 (e.154 ) (I e.155 ) (e.157 ) e.158 > ;
(s.172 e.154 ) (e.155 ) (e.157 ) e.158 = <F188 (e.154 ) (I I e.155 ) (e.157) e.158 > ;
}
* InputFormat: <F302 (e.154 ) (e.155 ) (e.157 ) e.158 >
F302 {
() (e.155 ) (e.157 ) e.158 = True ;
(r2 e.154 ) (e.155 ) (e.157 ) e.158 = <F312 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(r4 e.154 ) (e.155 ) (e.157 ) e.158 = <F268 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(r5 e.154 ) (e.155 ) (e.157 ) e.158 = <F288 (e.154 ) (I e.155 ) (e.157 ) e.158 > ;
(s.171 e.154 ) (e.155 ) (e.157 ) e.158 = <F188 (e.154 ) (I e.155 ) (I e.157 ) e.158 > ;
}
* InputFormat: <F288 (e.154 ) (e.155 ) (e.157 ) e.158 >
F288 {
() (e.155 ) (e.157 ) e.158 = True ;
(r1 e.154 ) () (e.157 ) I e.158 = <F199 (e.154 ) (I I e.157 ) e.158 > ;
(r2 e.154 ) (e.155 ) (e.157 ) e.158 = <F302 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(r4 e.154 ) (I e.155 ) (e.157 ) e.158 = <F268 (e.154 ) (e.155 ) (I e.157 ) e.158 > ;
(r5 e.154 ) (e.155 ) (e.157 ) e.158 = <F288 (e.154 ) (e.155 ) (I e.157 ) e.158 > ;
(s.169 e.154 ) (e.155 ) (e.157 ) e.158 = <F188 (e.154 ) (e.155 ) (I I e.157 ) e.158 > ;
}
* InputFormat: <F268 (e.154 ) (e.155 ) (e.157 ) e.158 >
F268 {
() (e.155 ) (e.157 ) e.158 = True ;
(r1 e.154 ) () (e.157 ) I e.158 = <F199 (e.154 ) (I e.157 ) e.158 > ;
(r2 e.154 ) (e.155 ) (e.157 ) e.158 = <F235 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(r4 e.154 ) (I e.155 ) (e.157 ) e.158 = <F248 (e.154 ) (e.155 ) (I e.157 ) e.158 > ;
(r5 e.154 ) (e.155 ) (e.157 ) e.158 = <F288 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(s.165 e.154 ) (e.155 ) (e.157 ) e.158 = <F188 (e.154 ) (e.155 ) (I e.157 ) e.158 > ;
}
* InputFormat: <F248 (e.154 ) (e.155 ) (e.157 ) e.158 >
F248 {
() (e.155 ) (e.157 ) e.158 = True ;
(r1 e.154 ) () (e.157 ) I e.158 = <F199 (e.154 ) (e.157 ) e.158 > ;
(r2 e.154 ) (e.155 ) (I e.157 ) e.158 = <F235 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(r4 e.154 ) (I e.155 ) (e.157 ) e.158 = <F248 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(r5 e.154 ) (e.155 ) (e.157 ) e.158 = <F268 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(s.161 e.154 ) (e.155 ) (e.157 ) e.158 = <F188 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
}
* InputFormat: <F235 (e.154 ) (e.155 ) (e.157 ) e.158 >
F235 {
() (e.155 ) (e.157 ) e.158 = True ;
(r2 e.154 ) (e.155 ) (I e.157 ) e.158 = <F235 (e.154 ) (I e.155 ) (e.157 ) e.158 > ;
(r4 e.154 ) (e.155 ) (e.157 ) e.158 = <F248 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(r5 e.154 ) (e.155 ) (e.157 ) e.158 = <F302 (e.154 ) (e.155 ) (e.157 ) e.158 > ;
(s.159 e.154 ) (e.155 ) (e.157 ) e.158 = <F188 (e.154 ) (I e.155 ) (e.157 ) e.158 > ;
}
* InputFormat: <F208 (e.143 ) (e.146 ) e.147 >
F208 {
() (e.146 ) e.147 = True ;
(r1 e.143 ) (e.146 ) I e.147 = <F199 (e.143 ) (e.146 ) e.147 > ;
(r2 e.143 ) (I e.146 ) e.147 = <F235 (e.143 ) () (e.146 ) e.147 > ;
(r5 ) (e.146 ) e.147 = True ;
(r5 r1 e.143 ) (e.146 ) I e.147 = <F199 (e.143 ) (I e.146 ) e.147 > ;
(r5 r2 ) (e.146 ) e.147 = True ;
(r5 r2 r2 e.143 ) (I e.146 ) e.147 = <F312 (e.143 ) () (e.146 ) e.147 > ;
(r5 r2 r4 e.143 ) (e.146 ) e.147 = <F208 (e.143 ) (e.146 ) e.147 > ;
(r5 r2 r5 e.143 ) (e.146 ) e.147 = <F302 (e.143 ) () (e.146 ) e.147 > ;
(r5 r2 s.189 e.143 ) (e.146 ) e.147 = <F188 (e.143 ) (I ) (e.146 ) e.147 > ;
(r5 r5 e.143 ) (e.146 ) e.147 = <F288 (e.143 ) () (e.146 ) e.147 > ;
(r5 s.187 e.143 ) (e.146 ) e.147 = <F188 (e.143 ) () (I e.146 ) e.147 > ;
(s.150 e.143 ) (e.146 ) e.147 = <F188 (e.143 ) () (e.146 ) e.147 > ;
}
* InputFormat: <F199 (e.143 ) (e.146 ) e.147 >
F199 {
() (e.146 ) e.147 = True ;
(r3 e.143 ) (e.146 ) e.147 = <F208 (e.143 ) (e.146 ) e.147 > ;
(r5 e.143 ) (e.146 ) e.147 = <F199 (e.143 ) (I e.146 ) e.147 > ;
(s.149 e.143 ) (e.146 ) e.147 = <F199 (e.143 ) (e.146 ) I e.147 > ;
}
* InputFormat: <F188 (e.143 ) (e.144 ) (e.146 ) e.147 >
F188 {
() (e.144 ) (e.146 ) e.147 = True ;
(r1 e.143 ) () (e.146 ) e.147 = <F199 (e.143 ) (e.146 ) e.147 > ;
(r2 e.143 ) (e.144 ) (I e.146 ) e.147 = <F188 (e.143 ) (I e.144 ) (e.146 ) e.147 > ;
(r4 e.143 ) (I e.144 ) (e.146 ) e.147 = <F188 (e.143 ) (e.144 ) (e.146 ) e.147 > ;
(r5 e.143 ) (e.144 ) (e.146 ) e.147 = <F188 (e.143 ) (e.144 ) (I e.146 ) e.147 > ;
(s.148 e.143 ) (e.144 ) (e.146 ) e.147 = <F188 (e.143 ) (e.144 ) (e.146 ) I e.147 > ;
}
* InputFormat: <F111 (e.118 ) (e.119 ) e.121 >
F111 {
() (e.119 ) e.121 = True ;
(r2 e.118 ) (e.119 ) I e.121 = <F98 (e.118 ) (e.119 ) e.121 > ;
(r4 e.118 ) (I e.119 ) e.121 = <F111 (e.118 ) (e.119 ) e.121 > ;
(r5 e.118 ) (e.119 ) e.121 = <F88 (e.118 ) (e.119 ) e.121 > ;
(s.125 e.118 ) (e.119 ) e.121 = <F188 (e.118 ) (e.119 ) (e.121 )> ;
}
* InputFormat: <F98 (e.118 ) (e.119 ) e.121 >
F98 {
() (e.119 ) e.121 = True ;
(r2 e.118 ) (e.119 ) I e.121 = <F98 (e.118 ) (I e.119 ) e.121 > ;
(r4 e.118 ) (e.119 ) e.121 = <F111 (e.118 ) (e.119 ) e.121 > ;
(r5 e.118 ) (e.119 ) e.121 = <F88 (e.118 ) (I e.119 ) e.121 > ;
(s.123 e.118 ) (e.119 ) e.121 = <F188 (e.118 ) (I e.119 ) (e.121 )> ;
}
* InputFormat: <F88 (e.118 ) (e.119 ) e.121 >
F88 {
() (e.119 ) e.121 = True ;
(r2 e.118 ) (e.119 ) e.121 = <F98 (e.118 ) (e.119 ) e.121 > ;
(r4 e.118 ) (I e.119 ) e.121 = <F88 (e.118 ) (e.119 ) e.121 > ;
(r5 e.118 ) (e.119 ) e.121 = <F88 (e.118 ) (e.119 ) I e.121 > ;
(s.122 e.118 ) (e.119 ) e.121 = <F188 (e.118 ) (e.119 ) (I e.121 )> ;
}
* InputFormat: <F56 (e.108 ) e.109 >
F56 {
() e.109 = True ;
(r4 e.108 ) I e.109 = <F56 (e.108 ) e.109 > ;
(r5 e.108 ) e.109 = <F88 (e.108 ) (e.109 )> ;
(s.112 e.108 ) e.109 = <F188 (e.108 ) (e.109 ) ()> ;
}
* InputFormat: <F47 (e.108 ) e.109 >
F47 {
() e.109 = True ;
(r4 e.108 ) e.109 = <F56 (e.108 ) e.109 > ;
(r5 e.108 ) e.109 = <F302 (e.108 ) (e.109 ) ()> ;
(s.111 e.108 ) e.109 = <F188 (e.108 ) (I e.109 ) ()> ;
}
* InputFormat: <F5 e.41 >
F5 {
= True ;
r5 = True ;
r5 r2 e.41 = <F47 (e.41 )> ;
r5 r5 e.41 = <F288 (e.41 ) () ()> ;
r5 s.103 e.41 = <F188 (e.41 ) () (I )> ;
s.102 e.41 = <F188 (e.41 ) () ()> ;
}
****************************** The End ************************************
|
Example #13 (Steve German's directory-based consistency protocol):
Model I
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.101 ) = True ;
reqS (e.101 ) = True ;
reqS s.103 e.41 (e.101 ) = <F17 (e.41 ) e.101 > ;
s.102 (e.101 ) = True ;
s.102 invS (e.101 ) = True ;
s.102 invS s.174 (e.101 ) = True ;
s.102 invS s.174 s.175 (e.101 ) = True ;
s.102 invS s.174 s.175 reqS (I e.101 ) = True ;
s.102 invS s.174 s.175 reqS s.177 e.41 (I e.101 ) = <F17 (e.41 ) I e.101 > ;
s.102 invS s.174 s.175 s.176 (I e.101 ) = True ;
s.102 invS s.174 s.175 s.176 invS (I e.101 ) = True ;
s.102 invS s.174 s.175 s.176 invS s.180 e.41 (I e.101 ) = <F179 (e.41 ) (e.101 )> ;
s.102 invS s.174 s.175 s.176 s.179 e.41 (I e.101 ) = <F165 (e.41 ) (e.101 )> ;
s.102 s.173 (e.101 ) = True ;
s.102 s.173 s.183 (e.101 ) = True ;
s.102 s.173 s.183 reqS (I e.101 ) = True ;
s.102 s.173 s.183 reqS s.185 e.41 (I e.101 ) = <F17 (e.41 ) I e.101 > ;
s.102 s.173 s.183 s.184 (I e.101 ) = True ;
s.102 s.173 s.183 s.184 invS (I e.101 ) = True ;
s.102 s.173 s.183 s.184 invS s.188 e.41 (I e.101 ) = <F179 (e.41 ) (e.101 )> ;
s.102 s.173 s.183 s.184 s.187 e.41 (I e.101 ) = <F165 (e.41 ) (e.101 )> ;
}
* InputFormat: <F179 (e.109 ) (e.110 ) e.111 >
F179 {
() (e.110 ) e.111 = True ;
(s.138 ) (e.110 ) e.111 = True ;
(s.138 reqS ) (e.110 ) e.111 = True ;
(s.138 reqS s.140 e.109 ) (e.110 ) e.111 = <F17 (e.109 ) I e.110 e.111 > ;
(s.138 s.139 ) (e.110 ) e.111 = True ;
(s.138 s.139 invS ) (e.110 ) e.111 = True ;
(s.138 s.139 invS s.143 e.109 ) (e.110 ) e.111 = <F179 (e.109 ) (e.110 ) e.111 > ;
(s.138 s.139 s.142 e.109 ) (e.110 ) e.111 = <F165 (e.109 ) (e.110 e.111 )> ;
}
* InputFormat: <F165 (e.109 ) (e.110 ) e.111 >
F165 {
() (e.110 ) e.111 = True ;
(invS ) (e.110 ) e.111 = True ;
(invS s.137 e.109 ) (e.110 ) e.111 = <F179 (e.109 ) (e.110 ) e.111 > ;
(servG e.109 ) (e.110 ) = <F179 (e.109 ) (e.110 )> ;
(s.136 e.109 ) (e.110 ) I e.111 = <F165 (e.109 ) (I e.110 ) e.111 > ;
}
* InputFormat: <F77 (e.109 ) (e.110 ) e.111 >
F77 {
() (e.110 ) e.111 = True ;
(s.118 ) (e.110 ) e.111 = True ;
(s.118 reqS ) (I e.110 ) e.111 = True ;
(s.118 reqS s.120 e.109 ) (I e.110 ) e.111 = <F17 (e.109 ) I e.110 I e.111 > ;
(s.118 reqS ) () e.111 = True ;
(s.118 reqS s.122 e.109 ) () e.111 = <F17 (e.109 ) I e.111 > ;
(s.118 reqE1 ) (I e.110 ) e.111 = True ;
(s.118 reqE1 invS ) (I e.110 ) e.111 = True ;
(s.118 reqE1 invS s.125 e.109 ) (I e.110 ) e.111 = <F77 (e.109 ) (I e.110 ) e.111 > ;
(s.118 reqE1 s.124 ) (I e.110 ) e.111 = True ;
(s.118 reqE1 s.124 invS e.109 ) (I e.110 ) e.111 = <F72 (e.109 ) (I e.110 ) e.111 > ;
(s.118 reqE1 s.124 s.127 e.109 ) (I e.110 ) e.111 = <F77 (e.109 ) (I e.110 ) e.111 > ;
(s.118 s.119 ) () e.111 = True ;
(s.118 s.119 invS ) () e.111 = True ;
(s.118 s.119 invS s.131 e.109 ) () e.111 = <F77 (e.109 ) () e.111 > ;
(s.118 s.119 s.130 ) () e.111 = True ;
(s.118 s.119 s.130 invS e.109 ) () e.111 = <F72 (e.109 ) () e.111 > ;
(s.118 s.119 s.130 s.133 e.109 ) () e.111 = <F77 (e.109 ) () e.111 > ;
}
* InputFormat: <F72 (e.109 ) (e.110 ) e.111 >
F72 {
() (e.110 ) e.111 = True ;
(s.117 e.109 ) (e.110 ) e.111 = <F77 (e.109 ) (e.110 ) e.111 > ;
}
* InputFormat: <F44 (e.109 ) (e.110 ) e.111 >
F44 {
() (e.110 ) e.111 = True ;
(reqS ) (I e.110 ) e.111 = True ;
(reqS s.113 ) (I e.110 ) e.111 = True ;
(reqS s.113 s.114 e.109 ) (I e.110 ) e.111 = <F44 (e.109 ) (e.110 ) I e.111 > ;
(reqE1 ) (I e.110 ) e.111 = True ;
(reqE1 invS e.109 ) (I e.110 ) e.111 = <F72 (e.109 ) (e.110 ) e.111 > ;
(reqE1 s.116 e.109 ) (I e.110 ) e.111 = <F165 (e.109 ) (e.110 ) e.111 > ;
(s.112 ) (e.110 ) e.111 = True ;
(s.112 invS ) (e.110 ) e.111 = True ;
(s.112 invS s.149 ) (e.110 ) e.111 = True ;
(s.112 invS s.149 s.150 ) (e.110 ) e.111 = True ;
(s.112 invS s.149 s.150 reqS ) (I e.110 ) e.111 = True ;
(s.112 invS s.149 s.150 reqS s.152 e.109) (I e.110) e.111 = <F17 (e.109) I e.110 e.111> ;
(s.112 invS s.149 s.150 reqS ) () I e.111 = True ;
(s.112 invS s.149 s.150 reqS s.154 e.109 ) () I e.111 = <F17 (e.109 ) I e.111 > ;
(s.112 invS s.149 s.150 reqE1 ) (I e.110 ) e.111 = True ;
(s.112 invS s.149 s.150 reqE1 invS ) (I e.110 ) e.111 = True ;
(s.112 invS s.149 s.150 reqE1 invS s.157 e.109 ) (I e.110 ) e.111
= <F179 (e.109 ) (e.110 ) e.111 > ;
(s.112 invS s.149 s.150 reqE1 s.156 e.109 ) (I e.110 ) e.111
= <F165 (e.109 ) (e.110 e.111 )> ;
(s.112 invS s.149 s.150 s.151 ) () I e.111 = True ;
(s.112 invS s.149 s.150 s.151 invS ) () I e.111 = True ;
(s.112 invS s.149 s.150 s.151 invS s.161 e.109 ) () I e.111 = <F77 (e.109 ) () e.111 > ;
(s.112 invS s.149 s.150 s.151 s.160 e.109 ) () I e.111 = <F165 (e.109 ) (e.111 )> ;
(s.112 servG ) (e.110 ) = True ;
(s.112 servG s.164 ) (e.110 ) = True ;
(s.112 servG s.164 reqS ) (I e.110 ) = True ;
(s.112 servG s.164 reqS s.166 e.109 ) (I e.110 ) = <F17 (e.109 ) I e.110 > ;
(s.112 servG s.164 s.165 ) (I e.110 ) = True ;
(s.112 servG s.164 s.165 invS ) (I e.110 ) = True ;
(s.112 servG s.164 s.165 invS s.169 e.109 ) (I e.110 ) = <F179 (e.109 ) (e.110 )> ;
(s.112 servG s.164 s.165 s.168 e.109 ) (I e.110 ) = <F165 (e.109 ) (e.110 )> ;
(s.112 s.148 e.109 ) (e.110 ) I e.111 = <F165 (e.109 ) (e.110 ) e.111 > ;
}
* InputFormat: <F17 (e.41 ) e.101 >
F17 {
() e.101 = True ;
(s.104 e.41 ) e.101 = <F44 (e.41 ) (e.101 )> ;
}
****************************** The End ************************************
|
Model B
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.101 ) = True ;
reqS (e.101 ) = True ;
reqS s.103 e.41 (e.101 ) = <F17 (e.41 ) e.101 > ;
s.102 (e.101 ) = True ;
s.102 s.144 (e.101 ) = True ;
s.102 s.144 s.145 e.41 (e.101 ) = <F143 (e.41 ) (e.101 )> ;
}
* InputFormat: <F143 (e.109 ) (e.110 ) e.111 >
F143 {
() (e.110 ) e.111 = True ;
(s.132 ) (e.110 ) e.111 = True ;
(s.132 reqS ) (I e.110 ) e.111 = True ;
(s.132 reqS s.134 e.109 ) (I e.110 ) e.111 = <F17 (e.109 ) I e.110 e.111 > ;
(s.132 reqS ) () I e.111 = True ;
(s.132 reqS s.136 e.109 ) () I e.111 = <F17 (e.109 ) I e.111 > ;
(s.132 reqE1 ) (I e.110 ) e.111 = True ;
(s.132 reqE1 s.138 ) (I e.110 ) e.111 = True ;
(s.132 reqE1 s.138 s.139 e.109 ) (I e.110 ) e.111 = <F143 (e.109 ) (I e.110 ) e.111 > ;
(s.132 s.133 ) () I e.111 = True ;
(s.132 s.133 s.141 ) () I e.111 = True ;
(s.132 s.133 s.141 s.142 e.109 ) () I e.111 = <F75 (e.109 ) () e.111 > ;
}
* InputFormat: <F75 (e.109 ) (e.110 ) e.111 >
F75 {
() (e.110 ) e.111 = True ;
(s.118 ) (e.110 ) e.111 = True ;
(s.118 reqS ) (I e.110 ) e.111 = True ;
(s.118 reqS s.120 e.109 ) (I e.110 ) e.111 = <F17 (e.109 ) I e.110 I e.111 > ;
(s.118 reqS ) () e.111 = True ;
(s.118 reqS s.122 e.109 ) () e.111 = <F17 (e.109 ) I e.111 > ;
(s.118 reqE1 ) (I e.110 ) e.111 = True ;
(s.118 reqE1 s.124 ) (I e.110 ) e.111 = True ;
(s.118 reqE1 s.124 s.125 e.109 ) (I e.110 ) e.111 = <F75 (e.109 ) (I e.110 ) e.111 > ;
(s.118 s.119 ) () e.111 = True ;
(s.118 s.119 s.127 ) () e.111 = True ;
(s.118 s.119 s.127 s.128 e.109 ) () e.111 = <F75 (e.109 ) () e.111 > ;
}
* InputFormat: <F44 (e.109 ) (e.110 ) e.111 >
F44 {
() (e.110 ) e.111 = True ;
(reqS ) (I e.110 ) e.111 = True ;
(reqS s.113 ) (I e.110 ) e.111 = True ;
(reqS s.113 s.114 e.109 ) (I e.110 ) e.111 = <F44 (e.109 ) (e.110 ) I e.111 > ;
(reqE1 ) (I e.110 ) e.111 = True ;
(reqE1 s.116 ) (I e.110 ) e.111 = True ;
(reqE1 s.116 s.117 e.109 ) (I e.110 ) e.111 = <F75 (e.109 ) (e.110 ) e.111 > ;
(s.112 ) (e.110 ) e.111 = True ;
(s.112 s.130 ) (e.110 ) e.111 = True ;
(s.112 s.130 s.131 e.109 ) (e.110 ) e.111 = <F143 (e.109 ) (e.110 ) e.111 > ;
}
* InputFormat: <F17 (e.41 ) e.101 >
F17 {
() e.101 = True ;
(s.104 e.41 ) e.101 = <F44 (e.41 ) (e.101 )> ;
}
****************************** The End ************************************
|
Example #14 (Load Balancing Monitor protocol):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
e.41 (e.101 ) = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F115 (e.146 ) (e.147 ) (e.148 ) (e.149 ) e.150 >
F115 {
(e.146 ) (I e.147 ) (I e.148 ) (e.149 ) e.150
= <F115 (e.146 ) (e.147 ) (e.148 ) (e.149 ) I e.150 > ;
() (e.147 ) () (e.149 ) e.150 = True ;
((s.153 ) e.146 ) (e.147 ) () (e.149 ) e.150 = <F24 (e.146 ) (e.149 e.147 ) e.150 > ;
() () (e.148 ) (e.149 ) e.150 = True ;
((s.157 ) e.146 ) () (e.148 ) (e.149 ) e.150 = <F24 (e.146 ) (e.149 ) e.150 > ;
}
* InputFormat: <F63 (e.123 ) (e.124 ) (e.125 ) (e.126 ) e.127 >
F63 {
(e.123 ) (I e.124 ) (I e.125 ) (e.126 ) e.127
= <F63 (e.123 ) (e.124 ) (e.125 ) (e.126 ) I e.127 > ;
() (e.124 ) () (e.126 ) e.127 = True ;
((s.130 ) e.123 ) (e.124 ) () (e.126 ) e.127 = <F24 (e.123 ) (I e.126 e.124 ) e.127 > ;
() () (e.125 ) (e.126 ) e.127 = True ;
((s.134 ) e.123 ) () (e.125 ) (e.126 ) e.127 = <F24 (e.123 ) (I e.126 ) e.127 > ;
}
* InputFormat: <F35 (e.109 ) (e.110 ) e.111 >
F35 {
() (e.110 ) e.111 = True ;
((r1 ) e.109 ) (e.110 ) e.111 = <F24 (e.109 ) (e.110 ) e.111 > ;
((r2 ) e.109 ) (e.110 ) I e.111 = <F35 (e.109 ) (I e.110 ) e.111 > ;
((s.118 (high_low I e.121 )) e.109 ) (e.110 ) I e.111
= <F63 (e.109 ) (e.111 ) (e.121 ) (e.110 )> ;
((s.118 (high_low ))) (e.110 ) e.111 = True ;
((s.118 (high_low )) (s.138 ) e.109 ) (e.110 ) e.111 = <F5 (e.109 ) I e.110 e.111 > ;
((s.118 (high_low e.121 ))) (e.110 ) = True ;
((s.118 (high_low e.121 )) (s.142 ) e.109 ) (e.110 ) = <F5 (e.109 ) I e.110 > ;
}
* InputFormat: <F24 (e.109 ) (e.110 ) e.111 >
F24 {
() (e.110 ) e.111 = True ;
((r1 ) e.109 ) (I e.110 ) e.111 = <F24 (e.109 ) (e.110 ) I e.111 > ;
((r2 ) e.109 ) (e.110 ) e.111 = <F35 (e.109 ) (e.110 ) e.111 > ;
((s.114 (high_low I e.144 )) e.109 ) (e.110 ) e.111 = <F115 (e.109 ) (e.111 ) (e.144 ) (e.110 )> ;
((s.114 (high_low ))) (e.110 ) e.111 = True ;
((s.114 (high_low )) (s.161 ) e.109 ) (e.110 ) e.111 = <F5 (e.109 ) e.110 I e.111 > ;
}
* InputFormat: <F5 (e.41 ) e.101 >
F5 {
() e.101 = True ;
((r1 ) e.41 ) I e.101 = <F24 (e.41 ) (e.101 )> ;
((s.104 (high_low ))) e.101 = True ;
((s.104 (high_low )) (s.166 ) e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
((s.104 (high_low e.163 ))) e.101 = True ;
((s.104 (high_low e.163 )) (s.170 ) e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
}
****************************** The End ************************************
|
Example #15 (Data Race Free Synchronization Model):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
e.41 (e.101 ) = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F41 (e.107 ) (e.108 ) e.109 >
F41 {
() (e.108 ) e.109 = True ;
(r1 ) (e.108 ) = True ;
(r1 s.113 e.107 ) (e.108 ) = <F5 (e.107 ) e.108 > ;
(r2 e.107 ) (e.108 ) e.109 = <F31 (e.107 ) (e.108 ) e.109 > ;
(s.112 e.107 ) (e.108 ) I e.109 = <F41 (e.107 ) (I e.108 ) e.109 > ;
}
* InputFormat: <F31 (e.107 ) (e.108 ) e.109 >
F31 {
() (e.108 ) e.109 = True ;
(r2 e.107 ) (I e.108 ) e.109 = <F31 (e.107 ) (e.108 ) I e.109 > ;
(s.110 e.107 ) (e.108 ) e.109 = <F41 (e.107 ) (e.108 ) e.109 > ;
}
* InputFormat: <F5 (e.41 ) e.101 >
F5 {
() e.101 = True ;
(r1 ) e.101 = True ;
(r1 s.103 e.41 ) e.101 = <F5 (e.41 ) e.101 > ;
(s.102 e.41 ) e.101 = <F31 (e.41 ) (e.101 )> ;
}
****************************** The End ************************************
|
Example #16 (Control Server Monitor protocol):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.101 ) = True ;
REQ e.41 (e.101 ) = <F24 (e.41 ) (e.101 )> ;
STOP e.41 (e.101 ) = <F1398 (e.41 ) (e.101 ) ()> ;
}
* InputFormat: <F24 (e.105 ) (e.106 ) e.107 >
F24 {
() (e.106 ) e.107 = True ;
(REQ e.105 ) (I e.106 ) e.107 = <F24 (e.105 ) (e.106 ) I e.107 > ;
(USE_C e.105 ) (e.106 ) e.107 = <F35 (e.105 ) (e.106 ) e.107 > ;
(STOP e.105 ) (e.106 ) e.107 = <F1373 (e.105 ) (e.106 ) (e.107 )> ;
}
* InputFormat: <F35 (e.105 ) (e.106 ) e.107 >
F35 {
() (e.106 ) e.107 = True ;
(REQ e.105 ) (I e.106 ) e.107 = <F35 (e.105 ) (e.106 ) I e.107 > ;
(RELEASE_C1 ) (e.106 ) e.107 = True ;
(RELEASE_C1 REQ e.105 ) (e.106 ) e.107 = <F24 (e.105 ) (e.106 ) e.107 > ;
(RELEASE_C1 USE_C e.105 ) (e.106 ) I e.107 = <F35 (e.105 ) (I e.106 ) e.107 > ;
(RELEASE_C1 STOP e.105 ) (e.106 ) e.107 = <F61 (e.105 ) (e.106 ) e.107 > ;
(RELEASE_C2 ) (e.106 ) e.107 = True ;
(RELEASE_C2 REQ e.105 ) (I e.106 ) e.107 = <F840 (e.105 ) (e.106 ) (e.107 )> ;
(RELEASE_C2 USE_C e.105 ) (e.106 ) I e.107 = <F852 (e.105 ) (e.106 ) (e.107 )> ;
(RELEASE_C2 USE_D e.105 ) (e.106 ) e.107 = <F1580 (e.105 ) (e.106 ) (e.107 )> ;
(RELEASE_C2 STOP e.105 ) (e.106 ) e.107 = <F127 (e.105 ) (e.106 ) (e.107 )> ;
(STOP e.105 ) (e.106 ) e.107 = <F1625 (e.105 ) (e.106 ) (e.107 )> ;
}
* InputFormat: <F61 (e.105 ) (e.106 ) e.107 >
F61 {
() (e.106 ) e.107 = True ;
(REQ e.105 ) (e.106 ) e.107 = <F69 (e.105 ) (e.106 ) e.107 > ;
(USE_C e.105 ) (e.106 ) I e.107 = <F232 (e.105 ) (e.106 ) (e.107 )> ;
(RETURN ) (e.106 ) e.107 = True ;
(RETURN REQ ) (e.106 ) e.107 = True ;
(RETURN REQ REQ e.105 ) (I e.106 ) e.107 = <F279 (e.105 ) (e.106 ) (e.107 )> ;
(RETURN REQ STOP e.105 ) (e.106 ) e.107 = <F1373 (e.105 ) (e.106 ) (e.107 )> ;
(RETURN STOP e.105 ) (e.106 ) e.107 = <F61 (e.105 ) (e.106 ) e.107 > ;
}
* InputFormat: <F69 (e.105 ) (e.106 ) e.107 >
F69 {
() (e.106 ) e.107 = True ;
(REQ e.105 ) (I e.106 ) e.107 = <F69 (e.105 ) (e.106 ) I e.107 > ;
(USE_C e.105 ) (e.106 ) e.107 = <F80 (e.105 ) (e.106 ) e.107 > ;
(RETURN ) (e.106 ) e.107 = True ;
(RETURN REQ e.105 ) (I e.106 ) e.107 = <F279 (e.105 ) (e.106 ) (e.107 )> ;
(RETURN STOP e.105 ) (e.106 ) e.107 = <F69 (e.105 ) (e.106 ) e.107 > ;
}
* InputFormat: <F80 (e.105 ) (e.106 ) e.107 >
F80 {
() (e.106 ) e.107 = True ;
(REQ e.105 ) (I e.106 ) e.107 = <F80 (e.105 ) (e.106 ) I e.107 > ;
(RELEASE_C1 e.105 ) (e.106 ) e.107 = <F61 (e.105 ) (e.106 ) e.107 > ;
(RELEASE_C2 e.105 ) (e.106 ) e.107 = <F127 (e.105 ) (e.106 ) (e.107 )> ;
(RETURN e.105 ) (e.106 ) e.107 = <F35 (e.105 ) (e.106 ) e.107 > ;
}
* InputFormat: <F127 (e.127 ) (e.128 ) (e.129 ) e.130 >
F127 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F139 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F1358 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F1721 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1721 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1721 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F1721 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F1690 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1358 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1358 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F158 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F1373 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F1690 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1690 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1690 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F1690 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_D ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D USE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F1690 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_D STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F1373 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F1358 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1373 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1373 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F195 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C ) (e.128 ) (e.129 ) e.130 = True ;
(USE_C REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F207 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130
= <F1398 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130
= <F127 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C USE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F158 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C RETURN e.127 ) (e.128 ) (e.129 ) e.130
= <F1495 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN ) (e.128 ) (e.129 ) e.130 = True ;
(RETURN REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN USE_D ) (e.128 ) (e.129 ) I e.130 = True ;
(RETURN USE_D REQ e.127 ) (I e.128 ) (e.129 ) I e.130
= <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN USE_D STOP e.127 ) (e.128 ) (e.129 ) I e.130
= <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F1373 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1495 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1495 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C1 REQ ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C1 REQ REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F402 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 REQ USE_C e.127 ) (e.128 ) (e.129 ) e.130
= <F1495 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 REQ USE_D ) (e.128 ) (e.129 ) I e.130 = True ;
(RELEASE_C1 REQ USE_D REQ e.127 ) (I e.128 ) (e.129 ) I e.130
= <F417 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 REQ USE_D USE_C e.127 ) (e.128 ) (e.129 ) I e.130
= <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 REQ USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F402 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 REQ USE_D STOP e.127 ) (e.128 ) (e.129 ) I e.130
= <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 REQ STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F1373 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 USE_C e.127 ) (e.128 ) (I e.129 ) e.130
= <F370 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 USE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F880 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F1398 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C2 REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F840 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_C e.127 ) (e.128 ) (I e.129 ) e.130
= <F852 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F1580 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F127 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F1625 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1625 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1625 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F1625 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D ) (e.128 ) (e.129 ) I e.130 = True ;
(USE_D REQ e.127 ) (I e.128 ) (e.129 ) I e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F1625 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D RETURN e.127 ) (e.128 ) (e.129 ) I e.130
= <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F1495 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1580 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1580 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F1580 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F1495 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D USE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F1580 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_D STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F1373 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F1358 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1398 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1398 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F1373 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F232 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F171 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN ) (e.128 ) (e.129 ) e.130 = True ;
(RETURN REQ ) (e.128 ) (e.129 ) e.130 = True ;
(RETURN REQ REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN REQ USE_D ) (e.128 ) (e.129 ) I e.130 = True ;
(RETURN REQ USE_D REQ e.127 ) (I e.128 ) (e.129 ) I e.130
= <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN REQ USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN REQ USE_D STOP e.127 ) (e.128 ) (e.129 ) I e.130
= <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN REQ STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F1373 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN USE_D ) (e.128 ) (e.129 ) I e.130 = True ;
(RETURN USE_D REQ ) (e.128 ) (e.129 ) I e.130 = True ;
(RETURN USE_D REQ REQ e.127 ) (I e.128 ) (e.129 ) I e.130
= <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN USE_D REQ RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN USE_D REQ STOP e.127 ) (e.128 ) (e.129 ) I e.130
= <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F271 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN USE_D STOP e.127 ) (e.128 ) (e.129 ) I e.130
= <F171 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F1398 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F139 (e.127 ) (e.128 ) (e.129 ) e.130 >
F139 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F139 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130
= <F127 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130
= <F127 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F158 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F852 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F158 (e.127 ) (e.128 ) (e.129 ) e.130 >
F158 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F158 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130
= <F171 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130
= <F935 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F207 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F171 (e.127 ) (e.128 ) (e.129 ) e.130 >
F171 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F158 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F220 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN ) (e.128 ) (e.129 ) e.130 = True ;
(RETURN REQ ) (e.128 ) (e.129 ) e.130 = True ;
(RETURN REQ REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN REQ RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN REQ STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F271 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F171 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F180 (e.127 ) (e.128 ) (e.129 ) e.130 >
F180 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F158 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F195 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN ) (e.128 ) (e.129 ) e.130 = True ;
(RETURN REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F195 (e.127 ) (e.128 ) (e.129 ) e.130 >
F195 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F195 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F207 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F180 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F207 (e.127 ) (e.128 ) (e.129 ) e.130 >
F207 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F207 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130 = <F220 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F158 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F220 (e.127 ) (e.128 ) (e.129 ) e.130 >
F220 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F195 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F232 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F171 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F271 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F232 (e.127 ) (e.128 ) (e.129 ) e.130 >
F232 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F207 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130 = <F245 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F158 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F370 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F370 (e.127 ) (e.128 ) (e.129 ) e.130 >
F370 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C1 REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F393 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 USE_C e.127 ) (e.128 ) (I e.129 ) e.130
= <F370 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 USE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F880 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F245 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C2 REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F840 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_C e.127 ) (e.128 ) (I e.129 ) e.130
= <F370 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_C2 USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F880 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F454 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F1226 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F1226 (e.127 ) (e.128 ) (e.129 ) e.130 >
F1226 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ ) (e.128 ) (e.129 ) e.130 = True ;
(REQ REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F654 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(REQ USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(REQ RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D ) (e.128 ) (e.129 ) I e.130 = True ;
(USE_D REQ e.127 ) (e.128 ) (e.129 ) I e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F1226 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D RETURN e.127 ) (e.128 ) (e.129 ) I e.130
= <F454 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F370 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F380 (e.127 ) (e.128 ) (e.129 ) e.130 >
F380 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130 = <F393 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130 = <F840 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F429 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP ) (e.128 ) (e.129 ) e.130 = True ;
(STOP REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F654 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F840 (e.127 ) (e.128 ) (e.129 ) e.130 >
F840 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F852 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D ) (e.128 ) (e.129 ) e.130 = True ;
(USE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F417 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
}
* InputFormat: <F852 (e.127 ) (e.128 ) (e.129 ) e.130 >
F852 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_C1 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C1 REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F840 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F370 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_C1 USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F880 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C2 REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F540 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F552 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_D ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C2 USE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F497 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_D USE_C e.127 ) (e.128 ) (I e.129 ) e.130
= <F509 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F840 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_D STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F935 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F127 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP ) (e.128 ) (e.129 ) e.130 = True ;
(STOP REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F632 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP USE_D ) (e.128 ) (e.129 ) e.130 = True ;
(STOP USE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP USE_D RELEASE_D ) (e.128 ) (e.129 ) e.130 = True ;
(STOP USE_D RELEASE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F654 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP USE_D RELEASE_D USE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP USE_D RELEASE_D RETURN e.127 ) (e.128 ) (e.129 ) e.130
= <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP USE_D RETURN e.127 ) (e.128 ) (e.129 ) e.130
= <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F852 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F880 (e.127 ) (e.128 ) (e.129 ) e.130 >
F880 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ ) (e.128 ) (e.129 ) e.130 = True ;
(REQ REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F417 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(REQ USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(REQ RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(REQ STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F454 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F393 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F171 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F901 (e.127 ) (e.128 ) (e.129 ) e.130 >
F901 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F429 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130 = <F880 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C2 REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F497 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F509 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F840 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F935 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP ) (e.128 ) (e.129 ) e.130 = True ;
(STOP REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP RELEASE_D ) (e.128 ) (e.129 ) e.130 = True ;
(STOP RELEASE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F654 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP RELEASE_D USE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP RELEASE_D RETURN e.127 ) (e.128 ) (e.129 ) e.130
= <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F901 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F935 (e.127 ) (e.128 ) (e.129 ) e.130 >
F935 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F158 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F953 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F953 (e.127 ) (e.128 ) (e.129 ) e.130 >
F953 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F953 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_D ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F279 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_D USE_D ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_D USE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D USE_D STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F180 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F127 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F935 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F393 (e.127 ) (e.128 ) (e.129 ) e.130 >
F393 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F370 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F442 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F220 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F402 (e.127 ) (e.128 ) (e.129 ) e.130 >
F402 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F417 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F195 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F417 (e.127 ) (e.128 ) (e.129 ) e.130 >
F417 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F417 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F429 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
}
* InputFormat: <F429 (e.127 ) (e.128 ) (e.129 ) e.130 >
F429 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F429 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130 = <F442 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130 = <F497 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F442 (e.127 ) (e.128 ) (e.129 ) e.130 >
F442 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F417 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F454 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F393 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F171 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
}
* InputFormat: <F454 (e.127 ) (e.128 ) (e.129 ) e.130 >
F454 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F429 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C1 REQ e.127 ) (e.128 ) (e.129 ) e.130
= <F442 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 USE_C e.127 ) (e.128 ) (I e.129 ) e.130
= <F454 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F393 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F171 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130 = <F488 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F370 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(STOP ) (e.128 ) (e.129 ) e.130 = True ;
(STOP REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP RELEASE_D ) (e.128 ) (e.129 ) e.130 = True ;
(STOP RELEASE_D REQ e.127 ) (e.128 ) (e.129 ) e.130
= <F654 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP RELEASE_D USE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F643 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(STOP RELEASE_D RETURN e.127 ) (e.128 ) (e.129 ) e.130
= <F370 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(STOP RETURN e.127 ) (e.128 ) (e.129 ) e.130
= <F454 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F488 (e.127 ) (e.128 ) (e.129 ) e.130 >
F488 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F497 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F454 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F393 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F171 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
}
* InputFormat: <F497 (e.127 ) (e.128 ) (e.129 ) e.130 >
F497 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F417 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F509 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
}
* InputFormat: <F509 (e.127 ) (e.128 ) (e.129 ) e.130 >
F509 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F429 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_C1 e.127 ) (e.128 ) (e.129 ) e.130 = <F488 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 e.127 ) (e.128 ) (e.129 ) e.130 = <F525 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F621 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F525 (e.127 ) (e.128 ) (e.129 ) e.130 >
F525 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F497 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F509 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F540 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F689 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F689 (e.127 ) (e.128 ) (e.129 ) e.130 >
F689 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (e.129 ) I I e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F158 (e.127 ) (e.128 ) (e.129 ) I I e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (e.128 ) (I e.129 ) I e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F707 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F707 (e.127 ) (e.128 ) (e.129 ) e.130 >
F707 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F707 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_D ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) I I e.130 > ;
(RELEASE_D USE_D ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_D USE_D REQ e.127 ) (I e.128 ) (e.129 ) e.130
= <F290 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_D USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130
= <F279 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_D USE_D STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F180 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_D STOP e.127 ) (e.128 ) (e.129 ) e.130
= <F127 (e.127 ) (e.128 ) (I e.129 ) I e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F689 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F540 (e.127 ) (e.128 ) (e.129 ) e.130 >
F540 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F402 (e.127 ) (e.128 ) (e.129 ) I I e.130 > ;
(USE_C e.127 ) (e.128 ) (e.129 ) e.130 = <F552 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F497 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (e.128 ) (I e.129 ) I e.130 > ;
}
* InputFormat: <F552 (e.127 ) (e.128 ) (e.129 ) e.130 >
F552 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) I I e.130 > ;
(RELEASE_C1 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C1 REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F540 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F370 (e.127 ) (e.128 ) (e.129 ) I I e.130 > ;
(RELEASE_C1 USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F488 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C1 STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (I e.128 ) (e.129 ) I e.130 > ;
(RELEASE_C2 ) (e.128 ) (e.129 ) e.130 = True ;
(RELEASE_C2 REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F540 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_C2 USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F552 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
(RELEASE_C2 USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F525 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RELEASE_C2 STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F127 (e.127 ) (e.128 ) (e.129 ) I I e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F509 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F610 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F610 (e.127 ) (e.128 ) (e.129 ) e.130 >
F610 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F610 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F621 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F552 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F621 (e.127 ) (e.128 ) (e.129 ) e.130 >
F621 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F621 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F632 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F509 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F632 (e.127 ) (e.128 ) (e.129 ) e.130 >
F632 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F632 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F643 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
}
* InputFormat: <F643 (e.127 ) (e.128 ) (e.129 ) e.130 >
F643 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F643 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F654 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F429 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F654 (e.127 ) (e.128 ) (e.129 ) e.130 >
F654 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F654 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F643 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F380 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
}
* InputFormat: <F245 (e.127 ) (e.128 ) (e.129 ) e.130 >
F245 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F220 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_C e.127 ) (e.128 ) (I e.129 ) e.130 = <F232 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F171 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(RETURN e.127 ) (e.128 ) (e.129 ) e.130 = <F263 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F263 (e.127 ) (e.128 ) (e.129 ) e.130 >
F263 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F271 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D ) (e.128 ) (e.129 ) I e.130 = True ;
(USE_D REQ ) (e.128 ) (e.129 ) I e.130 = True ;
(USE_D REQ REQ e.127 ) (e.128 ) (e.129 ) I e.130 = <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D REQ RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F279 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(USE_D REQ STOP e.127 ) (e.128 ) (e.129 ) I e.130
= <F171 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130
= <F263 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D STOP e.127 ) (e.128 ) (e.129 ) I e.130 = <F171 (e.127 ) (I e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F245 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F271 (e.127 ) (e.128 ) (e.129 ) e.130 >
F271 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (e.128 ) (e.129 ) e.130 = <F279 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D ) (e.128 ) (e.129 ) I e.130 = True ;
(USE_D REQ e.127 ) (e.128 ) (e.129 ) I e.130 = <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(USE_D RELEASE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F271 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D STOP e.127 ) (e.128 ) (e.129 ) I e.130 = <F171 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F220 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F279 (e.127 ) (e.128 ) (e.129 ) e.130 >
F279 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F279 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(USE_D e.127 ) (e.128 ) (e.129 ) I e.130 = <F290 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F195 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F290 (e.127 ) (e.128 ) (e.129 ) e.130 >
F290 {
() (e.128 ) (e.129 ) e.130 = True ;
(REQ e.127 ) (I e.128 ) (e.129 ) e.130 = <F290 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(RELEASE_D e.127 ) (e.128 ) (e.129 ) e.130 = <F279 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(STOP e.127 ) (e.128 ) (e.129 ) e.130 = <F180 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
}
****************************** The End ************************************
|
Example #17 (Inc/Dec):
The result of supercompilation of the fragment
of the parameterized
"Atomic Increments and decrements on a Point object" protocol violating a safety property.
The incorrect model of the parameterized
"Atomic Increments and decrements on a Point object" protocol
is taken
from the web-page by Laurent van Begin.
*$MST_FROM_ENTRY;
*$STRATEGY Applicative ;
*$LENGTH 0 ;
*$MATCHING ForRepeatedSpecialization ;
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.102 ) (e.101 ) = True ;
r1 e.41 (e.102 ) (e.101 ) = <F21 (e.41 ) (e.102 )> ;
}
* InputFormat: <F141 (e.127 ) (e.128 ) (e.129 ) e.130 >
F141 {
() (e.128 ) (e.129 ) I e.130 = False3 ;
() (e.128 ) (e.129 ) e.130 = True ;
(r1 e.127 ) (I e.128 ) (e.129 ) e.130 = <F141 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(r5 e.127 ) (e.128 ) (e.129 ) e.130 = <F105 (e.127 ) (e.128 ) (e.129 ) I e.130 > ;
}
* InputFormat: <F129 (e.127 ) (e.128 ) (e.129 ) e.130 >
F129 {
() (e.128 ) (e.129 ) I e.130 = False3 ;
() (e.128 ) (e.129 ) e.130 = True ;
(r1 e.127 ) (I e.128 ) (e.129 ) e.130 = <F129 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(r4 e.127 ) (e.128 ) (e.129 ) e.130 = <F141 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F117 (e.127 ) (e.128 ) (e.129 ) e.130 >
F117 {
() (e.128 ) (e.129 ) I e.130 = False3 ;
() (e.128 ) (e.129 ) e.130 = True ;
(r1 e.127 ) (I e.128 ) (e.129 ) e.130 = <F117 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(r3 e.127 ) (e.128 ) (e.129 ) e.130 = <F129 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F105 (e.127 ) (e.128 ) (e.129 ) e.130 >
F105 {
() (e.128 ) (e.129 ) I e.130 = False3 ;
() (e.128 ) (e.129 ) e.130 = True ;
(r1 e.127 ) (I e.128 ) (e.129 ) e.130 = <F105 (e.127 ) (e.128 ) (I e.129 ) e.130 > ;
(r2 e.127 ) (e.128 ) (I e.129 ) e.130 = <F117 (e.127 ) (e.128 ) (e.129 ) e.130 > ;
}
* InputFormat: <F51 (e.106 ) (e.107 ) e.108 >
F51 {
() (e.107 ) e.108 = True ;
(r1 e.106 ) (I e.107 ) e.108 = <F51 (e.106 ) (e.107 ) I e.108 > ;
(r5 e.106 ) (e.107 ) e.108 = <F105 (e.106 ) (e.107 ) (e.108 )> ;
}
* InputFormat: <F41 (e.106 ) (e.107 ) e.108 >
F41 {
() (e.107 ) e.108 = True ;
(r1 e.106 ) (I e.107 ) e.108 = <F41 (e.106 ) (e.107 ) I e.108 > ;
(r4 e.106 ) (e.107 ) e.108 = <F51 (e.106 ) (e.107 ) e.108 > ;
}
* InputFormat: <F31 (e.106 ) (e.107 ) e.108 >
F31 {
() (e.107 ) e.108 = True ;
(r1 e.106 ) (I e.107 ) e.108 = <F31 (e.106 ) (e.107 ) I e.108 > ;
(r3 e.106 ) (e.107 ) e.108 = <F41 (e.106 ) (e.107 ) e.108 > ;
}
* InputFormat: <F21 (e.106 ) (e.107 ) e.108 >
F21 {
() (e.107 ) e.108 = True ;
(r1 e.106 ) (I e.107 ) e.108 = <F21 (e.106 ) (e.107 ) I e.108 > ;
(r2 e.106 ) (e.107 ) e.108 = <F31 (e.106 ) (e.107 ) e.108 > ;
}
****************************** The End ************************************
|
Example #18 (P/C):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.102 ) (e.101 ) = True ;
c1 e.41 (e.102 ) (e.101 ) = <F24 (e.41 ) (e.102 ) () e.101 > ;
s.103 e.41 (e.102 ) (e.101 ) = <F341 (e.41 ) (e.102 ) e.101 > ;
}
* InputFormat: <F341 (e.209 ) (e.210 ) e.211 >
F341 {
() (e.210 ) e.211 = True ;
(c1 e.209 ) (e.210 ) e.211 = <F294 (e.209 ) (e.210 ) () e.211 > ;
(p1 e.209 ) (e.210 ) I e.211 = <F341 (e.209 ) (e.210 ) e.211 > ;
(s.213 e.209 ) (e.210 ) e.211 = True ;
}
* InputFormat: <F294 (e.194 ) (e.195 ) (e.196 ) e.197 >
F294 {
() (e.195 ) (e.196 ) e.197 = True ;
(c1 e.194 ) (I e.195 ) (e.196 ) e.197 = <F294 (e.194 ) (e.195 ) (I e.196 ) e.197 > ;
(c2 e.194 ) (e.195 ) (e.196 ) e.197 = <F258 (e.194 ) (e.195 ) (e.196 ) e.197 > ;
(p1 e.194 ) (e.195 ) (e.196 ) I e.197 = <F294 (e.194 ) (e.195 ) (e.196 ) e.197 > ;
(s.199 e.194 ) (e.195 ) (e.196 ) e.197 = True ;
}
* InputFormat: <F258 (e.181 ) (e.182 ) (e.183 ) e.184 >
F258 {
() (e.182 ) (e.183 ) e.184 = True ;
(c1 e.181 ) (I e.182 ) (e.183 ) e.184 = <F258 (e.181 ) (e.182 ) (I e.183 ) e.184 > ;
(c3 e.181 ) (e.182 ) (e.183 ) e.184 = <F208 (e.181 ) (e.182 ) (e.183 ) e.184 > ;
(s.186 e.181 ) (e.182 ) (e.183 ) I e.184 = <F258 (e.181 ) (e.182 ) (e.183 ) e.184 > ;
}
* InputFormat: <F208 (e.164 ) (e.165 ) (e.166 ) e.168 >
F208 {
() (e.165 ) (e.166 ) e.168 = True ;
(c1 e.164 ) (I e.165 ) (e.166 ) e.168 = <F208 (e.164 ) (e.165 ) (I e.166 ) e.168 > ;
(c2 e.164 ) (e.165 ) (I e.166 ) e.168 = <F143 (e.164 ) (e.165 ) (e.166 ) e.168 > ;
(p1 e.164 ) (e.165 ) (e.166 ) I e.168 = <F208 (e.164 ) (e.165 ) (e.166 ) e.168 > ;
(s.170 e.164 ) (e.165 ) (e.166 ) e.168 = True ;
}
* InputFormat: <F154 (e.144 ) (e.145 ) (e.146 ) e.148 >
F154 {
() (e.145 ) (e.146 ) e.148 = True ;
(c1 e.144 ) (I e.145 ) (e.146 ) e.148 = <F154 (e.144 ) (e.145 ) (I e.146 ) e.148 > ;
(c2 e.144 ) (e.145 ) (I e.146 ) e.148 = <F143 (e.144 ) (e.145 ) (e.146 ) e.148 > ;
(p1 e.144 ) (e.145 ) (e.146 ) I e.148 = <F154 (e.144 ) (e.145 ) (e.146 ) e.148 > ;
(s.152 e.144 ) (e.145 ) (e.146 ) e.148 = True ;
}
* InputFormat: <F143 (e.144 ) (e.145 ) (e.146 ) e.148 >
F143 {
() (e.145 ) (e.146 ) e.148 = True ;
(c1 e.144 ) (I e.145 ) (e.146 ) e.148 = <F143 (e.144 ) (e.145 ) (I e.146 ) e.148 > ;
(c3 e.144 ) (e.145 ) (e.146 ) e.148 = <F154 (e.144 ) (e.145 ) (e.146 ) e.148 > ;
(s.150 e.144 ) (e.145 ) (e.146 ) I e.148 = <F143 (e.144 ) (e.145 ) (e.146 ) e.148 > ;
}
* InputFormat: <F83 (e.119 ) (e.120 ) (e.121 ) e.123 >
F83 {
() (e.120 ) (e.121 ) e.123 = True ;
(c1 e.119 ) (I e.120 ) (e.121 ) e.123 = <F83 (e.119 ) (e.120 ) (I e.121 ) e.123 > ;
(c3 e.119 ) (e.120 ) (e.121 ) e.123 = <F72 (e.119 ) (e.120 ) (e.121 ) e.123 > ;
(s.126 e.119 ) (e.120 ) (e.121 ) e.123 = <F143 (e.119 ) (e.120 ) (e.121 ) e.123 > ;
}
* InputFormat: <F72 (e.119 ) (e.120 ) (e.121 ) e.123 >
F72 {
() (e.120 ) (e.121 ) e.123 = True ;
(c1 e.119 ) (I e.120 ) (e.121 ) e.123 = <F72 (e.119 ) (e.120 ) (I e.121 ) e.123 > ;
(c2 e.119 ) (e.120 ) (I e.121 ) e.123 = <F83 (e.119 ) (e.120 ) (e.121 ) e.123 > ;
(s.124 e.119 ) (e.120 ) (e.121 ) e.123 = <F208 (e.119 ) (e.120 ) (e.121 ) e.123 > ;
}
* InputFormat: <F35 (e.106 ) (e.107 ) (e.108 ) e.109 >
F35 {
() (e.107 ) (e.108 ) e.109 = True ;
(c1 e.106 ) (I e.107 ) (e.108 ) e.109 = <F35 (e.106 ) (e.107 ) (I e.108 ) e.109 > ;
(c3 e.106 ) (e.107 ) (e.108 ) e.109 = <F72 (e.106 ) (e.107 ) (e.108 ) e.109 > ;
(s.112 e.106 ) (e.107 ) (e.108 ) e.109 = <F258 (e.106 ) (e.107 ) (e.108 ) e.109 > ;
}
* InputFormat: <F24 (e.106 ) (e.107 ) (e.108 ) e.109 >
F24 {
() (e.107 ) (e.108 ) e.109 = True ;
(c1 e.106 ) (I e.107 ) (e.108 ) e.109 = <F24 (e.106 ) (e.107 ) (I e.108 ) e.109 > ;
(c2 e.106 ) (e.107 ) (e.108 ) e.109 = <F35 (e.106 ) (e.107 ) (e.108 ) e.109 > ;
(s.110 e.106 ) (e.107 ) (e.108 ) e.109 = <F294 (e.106 ) (e.107 ) (e.108 ) e.109 > ;
}
****************************** The End ************************************
|
Example #19 (P/C2sansinv):
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
(e.102 ) (e.101 ) = True ;
c1 e.41 (e.102 ) (e.101 ) = <F33 (e.41 ) (e.102 ) e.101 > ;
s.103 e.41 (e.102 ) (e.101 ) = <F1214 (e.41 ) (e.102 ) (e.101 )> ;
}
* InputFormat: <F1390 (e.351 ) (e.352 ) (e.353 ) e.354 >
F1390 {
() (e.352 ) (e.353 ) e.354 = True ;
(c1 e.351 ) (e.352 ) (e.353 ) e.354 = <F1032 (e.351 ) (e.352 ) (e.353 ) e.354 > ;
(p1 e.351 ) (e.352 ) (I e.353 ) e.354 = <F1390 (e.351 ) (e.352 ) (e.353 ) I e.354 > ;
(s.359 e.351 ) (e.352 ) (e.353 ) I e.354 = <F1371 (e.351 ) (e.352 ) (e.353 ) e.354 > ;
}
* InputFormat: <F1371 (e.351 ) (e.352 ) (e.353 ) e.354 >
F1371 {
() (e.352 ) (e.353 ) e.354 = True ;
(c1 e.351 ) (e.352 ) (e.353 ) e.354 = <F1013 (e.351 ) (e.352 ) (e.353 ) e.354 > ;
(p1 e.351 ) (e.352 ) (I e.353 ) e.354 = <F1371 (e.351 ) (e.352 ) (e.353 ) I e.354 > ;
(s.356 e.351 ) (e.352 ) (e.353 ) e.354 = <F1390 (e.351 ) (e.352 ) (e.353 ) e.354 > ;
}
* InputFormat: <F1309 (e.322 ) (e.323 ) (e.324 ) e.325 >
F1309 {
() (e.323 ) (e.324 ) e.325 = True ;
(c1 e.322 ) (e.323 ) (e.324 ) e.325 = <F742 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
(p1 e.322 ) (e.323 ) (I e.324 ) e.325 = <F1309 (e.322 ) (e.323 ) (e.324 ) I e.325 > ;
(s.341 e.322 ) (e.323 ) (e.324 ) e.325 = <F1371 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
}
* InputFormat: <F1290 (e.322 ) (e.323 ) (e.324 ) e.325 >
F1290 {
() (e.323 ) (e.324 ) e.325 = True ;
(c1 e.322 ) (e.323 ) (e.324 ) e.325 = <F723 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
(p1 e.322 ) (e.323 ) (I e.324 ) e.325 = <F1290 (e.322 ) (e.323 ) (e.324 ) I e.325 > ;
(s.338 e.322 ) (e.323 ) (e.324 ) e.325 = <F1309 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
}
* InputFormat: <F1271 (e.322 ) (e.323 ) (e.324 ) e.325 >
F1271 {
() (e.323 ) (e.324 ) e.325 = True ;
(c1 e.322 ) (e.323 ) (e.324 ) e.325 = <F704 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
(p1 e.322 ) (e.323 ) (I e.324 ) e.325 = <F1271 (e.322 ) (e.323 ) (e.324 ) I e.325 > ;
(s.335 e.322 ) (e.323 ) (e.324 ) e.325 = <F1290 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
}
* InputFormat: <F1252 (e.322 ) (e.323 ) (e.324 ) e.325 >
F1252 {
() (e.323 ) (e.324 ) e.325 = True ;
(c1 e.322 ) (e.323 ) (e.324 ) e.325 = <F685 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
(p1 e.322 ) (e.323 ) (I e.324 ) e.325 = <F1252 (e.322 ) (e.323 ) (e.324 ) I e.325 > ;
(s.332 e.322 ) (e.323 ) (e.324 ) e.325 = <F1271 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
}
* InputFormat: <F1233 (e.322 ) (e.323 ) (e.324 ) e.325 >
F1233 {
() (e.323 ) (e.324 ) e.325 = True ;
(c1 e.322 ) (e.323 ) (e.324 ) e.325 = <F666 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
(p1 e.322 ) (e.323 ) (I e.324 ) e.325 = <F1233 (e.322 ) (e.323 ) (e.324 ) I e.325 > ;
(s.329 e.322 ) (e.323 ) (e.324 ) e.325 = <F1252 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
}
* InputFormat: <F1214 (e.322 ) (e.323 ) (e.324 ) e.325 >
F1214 {
() (e.323 ) (e.324 ) e.325 = True ;
(c1 e.322 ) (e.323 ) (e.324 ) e.325 = <F626 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
(p1 e.322 ) (e.323 ) (I e.324 ) e.325 = <F1214 (e.322 ) (e.323 ) (e.324 ) I e.325 > ;
(s.326 e.322 ) (e.323 ) (e.324 ) e.325 = <F1233 (e.322 ) (e.323 ) (e.324 ) e.325 > ;
}
* InputFormat: <F1109 (e.282 ) (e.283 ) (e.285 ) e.286 >
F1109 {
() (e.283 ) (e.285 ) e.286 = True ;
(c1 e.282 ) (I e.283 ) (e.285 ) e.286 = <F1109 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(c2 e.282 ) (e.283 ) (e.285 ) e.286 = True ;
(p1 e.282 ) (e.283 ) (I e.285 ) e.286 = <F626 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(p2 e.282 ) (e.283 ) (e.285 ) I e.286 = <F666 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(s.302 e.282 ) (e.283 ) (e.285 ) e.286 = <F666 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
}
* InputFormat: <F1094 (e.282 ) (e.283 ) (e.285 ) e.286 >
F1094 {
() (e.283 ) (e.285 ) e.286 = True ;
(c1 e.282 ) (I e.283 ) (e.285 ) e.286 = <F1094 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(c8 e.282 ) (e.283 ) (e.285 ) e.286 = <F1109 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(s.300 e.282 ) (e.283 ) (I e.285 ) e.286 = <F804 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
}
* InputFormat: <F1079 (e.282 ) (e.283 ) (e.285 ) e.286 >
F1079 {
() (e.283 ) (e.285 ) e.286 = True ;
(c1 e.282 ) (I e.283 ) (e.285 ) e.286 = <F1079 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(c7 e.282 ) (e.283 ) (e.285 ) e.286 = <F1094 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(s.298 e.282 ) (e.283 ) (I e.285 ) e.286 = <F1079 (e.282 ) (e.283 ) (e.285 ) I e.286 > ;
}
* InputFormat: <F1064 (e.282 ) (e.283 ) (e.285 ) e.286 >
F1064 {
() (e.283 ) (e.285 ) e.286 = True ;
(c1 e.282 ) (I e.283 ) (e.285 ) e.286 = <F1064 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(c6 e.282 ) (e.283 ) (e.285 ) e.286 = <F1079 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(s.296 e.282 ) (e.283 ) (I e.285 ) e.286 = <F1064 (e.282 ) (e.283 ) (e.285 ) I e.286 > ;
}
* InputFormat: <F1049 (e.282 ) (e.283 ) (e.285 ) e.286 >
F1049 {
() (e.283 ) (e.285 ) e.286 = True ;
(c1 e.282 ) (I e.283 ) (e.285 ) e.286 = <F1049 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(c5 e.282 ) (e.283 ) (e.285 ) e.286 = <F1064 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(s.294 e.282 ) (e.283 ) (I e.285 ) e.286 = <F1049 (e.282 ) (e.283 ) (e.285 ) I e.286 > ;
}
* InputFormat: <F1032 (e.282 ) (e.283 ) (e.285 ) e.286 >
F1032 {
() (e.283 ) (e.285 ) e.286 = True ;
(c1 e.282 ) (I e.283 ) (e.285 ) e.286 = <F1032 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(c2 e.282 ) (e.283 ) (e.285 ) e.286 = <F1049 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(p1 e.282 ) (e.283 ) (I e.285 ) e.286 = <F1032 (e.282 ) (e.283 ) (e.285 ) I e.286 > ;
(p2 e.282 ) (e.283 ) (e.285 ) I e.286 = <F1013 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(s.292 e.282 ) (e.283 ) (e.285 ) e.286 = <F1013 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
}
* InputFormat: <F1013 (e.282 ) (e.283 ) (e.285 ) e.286 >
F1013 {
() (e.283 ) (e.285 ) e.286 = True ;
(c1 e.282 ) (I e.283 ) (e.285 ) e.286 = <F1013 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
(p1 e.282 ) (e.283 ) (I e.285 ) e.286 = <F1013 (e.282 ) (e.283 ) (e.285 ) I e.286 > ;
(s.289 e.282 ) (e.283 ) (e.285 ) e.286 = <F1032 (e.282 ) (e.283 ) (e.285 ) e.286 > ;
}
* InputFormat: <F804 (e.215 ) (e.216 ) (e.218 ) e.219 >
F804 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F804 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(c8 e.215 ) (e.216 ) (e.218 ) e.219 = <F626 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(s.247 e.215 ) (e.216 ) (I e.218 ) e.219 = <F804 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
}
* InputFormat: <F789 (e.215 ) (e.216 ) (e.218 ) e.219 >
F789 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F789 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(c7 e.215 ) (e.216 ) (e.218 ) e.219 = <F804 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(s.245 e.215 ) (e.216 ) (I e.218 ) e.219 = <F789 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
}
* InputFormat: <F774 (e.215 ) (e.216 ) (e.218 ) e.219 >
F774 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F774 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(c6 e.215 ) (e.216 ) (e.218 ) e.219 = <F789 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(s.243 e.215 ) (e.216 ) (I e.218 ) e.219 = <F774 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
}
* InputFormat: <F759 (e.215 ) (e.216 ) (e.218 ) e.219 >
F759 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F759 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(c5 e.215 ) (e.216 ) (e.218 ) e.219 = <F774 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(s.241 e.215 ) (e.216 ) (I e.218 ) e.219 = <F759 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
}
* InputFormat: <F742 (e.215 ) (e.216 ) (e.218 ) e.219 >
F742 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F742 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(c2 e.215 ) (e.216 ) (e.218 ) e.219 = <F759 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(p1 e.215 ) (e.216 ) (I e.218 ) e.219 = <F742 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
(p2 e.215 ) (e.216 ) (e.218 ) e.219 = <F1013 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(s.239 e.215 ) (e.216 ) (e.218 ) e.219 = <F1013 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
}
* InputFormat: <F723 (e.215 ) (e.216 ) (e.218 ) e.219 >
F723 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F723 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(p1 e.215 ) (e.216 ) (I e.218 ) e.219 = <F723 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
(s.236 e.215 ) (e.216 ) (e.218 ) e.219 = <F742 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
}
* InputFormat: <F704 (e.215 ) (e.216 ) (e.218 ) e.219 >
F704 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F704 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(p1 e.215 ) (e.216 ) (I e.218 ) e.219 = <F704 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
(s.233 e.215 ) (e.216 ) (e.218 ) e.219 = <F723 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
}
* InputFormat: <F685 (e.215 ) (e.216 ) (e.218 ) e.219 >
F685 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F685 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(p1 e.215 ) (e.216 ) (I e.218 ) e.219 = <F685 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
(s.230 e.215 ) (e.216 ) (e.218 ) e.219 = <F704 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
}
* InputFormat: <F666 (e.215 ) (e.216 ) (e.218 ) e.219 >
F666 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F666 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(p1 e.215 ) (e.216 ) (I e.218 ) e.219 = <F666 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
(s.227 e.215 ) (e.216 ) (e.218 ) e.219 = <F685 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
}
* InputFormat: <F626 (e.215 ) (e.216 ) (e.218 ) e.219 >
F626 {
() (e.216 ) (e.218 ) e.219 = True ;
(c1 e.215 ) (I e.216 ) (e.218 ) e.219 = <F626 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(c2 e.215 ) (e.216 ) (e.218 ) e.219 = True ;
(p1 e.215 ) (e.216 ) (I e.218 ) e.219 = <F626 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
(p2 e.215 ) (e.216 ) (e.218 ) e.219 = <F666 (e.215 ) (e.216 ) (e.218 ) e.219 > ;
(s.221 e.215 ) (e.216 ) (e.218 ) e.219 = <F666 (e.215 ) (e.216 ) (e.218 ) I e.219 > ;
}
* InputFormat: <F33 (e.106 ) (e.107 ) e.109 >
F33 {
() (e.107 ) e.109 = True ;
(c1 e.106 ) (I e.107 ) e.109 = <F33 (e.106 ) (e.107 ) e.109 > ;
(c2 e.106 ) (e.107 ) e.109 = True ;
(s.110 e.106 ) (e.107 ) e.109 = <F626 (e.106 ) (e.107 ) (e.109 )> ;
}
****************************** The End ************************************
Example #20 (2P/2C):
The residual program is too large and may be
downloaded.
Example #21 (SPS2):
The result of supercompilation of
the incorrect specification
of the parameterized SPS2 protocol taken from
the paper by
X. Zhao, K. Sammut, F. He, Sh. Qin and made more precise
(but still incorrect)
by Xuemei Zhao in
an e-mail message.
/*
$ENTRY Go {
= <Prout <Go e.1 >> ;
}
*/
* InputFormat: <Go e.41 >
$ENTRY Go {
e.41 (e.101 ) = <F5 (e.41 ) e.101 > ;
}
* InputFormat: <F5 (e.41 ) e.101 >
F5 {
() e.101 = True ;
(r2 e.41 ) e.101 = <F27 (e.41 ) (e.101 )> ;
(wm13 e.41 ) e.101 = <F41 (e.41 ) (e.101 )> ;
}
* InputFormat: <F27 (e.105 ) (e.106 ) e.107 >
F27 {
() (e.106 ) e.107 = True ;
(r5 e.105 ) (I e.106 ) e.107 = <F27 (e.105 ) (e.106 ) I e.107 > ;
(wm12 e.105 ) (e.106 ) e.107 = <F41 (e.105 ) (e.106 ) e.107 > ;
(wm14 e.105 ) (I e.106 ) e.107 = <F41 (e.105 ) (e.106 ) I e.107 > ;
(rp1-r17 ) (e.106 ) e.107 = True ;
(rp1-r17 r5 e.105 ) (e.106 ) e.107 = <F27 (e.105 ) (e.106 ) e.107 > ;
(rp1-r17 wm12 e.105 ) (e.106 ) I e.107 = <F41 (e.105 ) (I e.106 ) e.107 > ;
(rp1-r17 wm14 e.105 ) (e.106 ) e.107 = <F41 (e.105 ) (e.106 ) e.107 > ;
(rp1-r17 rp1-r17 e.105 ) (e.106 ) I e.107 = <F956 (e.105 ) (e.106 ) e.107 > ;
(rp1-r17 repS-r21 ) (e.106 ) e.107 = True ;
(rp1-r17 repS-r21 r2 e.105 ) (e.106 ) e.107 = <F27 (e.105 ) (e.106 ) e.107 > ;
(rp1-r17 repS-r21 r5 e.105 ) (I e.106 ) e.107 = <F748 (e.105 ) () (e.106 ) e.107 > ;
(rp1-r17 repS-r21 wm12 e.105 ) (e.106 ) I e.107 = <F41 (e.105 ) (I e.106 ) e.107 > ;
(rp1-r17 repS-r21 wm13 e.105 ) (e.106 ) e.107 = <F41 (e.105 ) (e.106 ) e.107 > ;
(rp1-r17 repS-r21 wm14 e.105 ) (I e.106 ) e.107 = <F41 (e.105 ) (I e.106 ) e.107 > ;
(rp1-r17 repS-r21 rp1-r17 e.105 ) (e.106 ) I e.107 = <F732 (e.105 ) () (e.106 ) e.107 > ;
(rp1-r17 repS-r21 repS-r21 e.105 ) (I e.106 ) e.107 = <F782 (e.105 ) () (e.106 ) e.107 > ;
(rp1-r17 repS-r21 repS-r22 e.105 ) (e.106 ) I e.107 = <F782 (e.105 ) () (e.106 ) e.107 > ;
(rp1-r17 repS-r22 e.105 ) (e.106 ) I e.107 = <F732 (e.105 ) () (e.106 ) e.107 > ;
(repS-r21 e.105 ) (I e.106 ) e.107 = <F748 (e.105 ) () (e.106 ) e.107 > ;
(repS-r22 ) (e.106 ) e.107 = True ;
(repS-r22 r2 e.105 ) (e.106 ) e.107 = <F27 (e.105 ) (e.106 ) e.107 > ;
(repS-r22 r5 e.105 ) (I e.106 ) e.107 = <F748 (e.105 ) () (e.106 ) e.107 > ;
(repS-r22 wm12 e.105 ) (e.106 ) I e.107 = <F41 (e.105 ) (I e.106 ) e.107 > ;
(repS-r22 wm13 e.105 ) (e.106 ) e.107 = <F41 (e.105 ) (e.106 ) e.107 > ;
(repS-r22 wm14 e.105 ) (I e.106 ) e.107 = <F41 (e.105 ) (I e.106 ) e.107 > ;
(repS-r22 rp1-r17 e.105 ) (e.106 ) I e.107 = <F732 (e.105 ) () (e.106 ) e.107 > ;
(repS-r22 repS-r21 e.105 ) (I e.106 ) e.107 = <F782 (e.105 ) () (e.106 ) e.107 > ;
(repS-r22 repS-r22 e.105 ) (e.106 ) I e.107 = <F782 (e.105 ) () (e.106 ) e.107 > ;
}
* InputFormat: <F41 (e.105 ) (e.106 ) e.107 >
F41 {
() (e.106 ) e.107 = True ;
(r3 e.105 ) (I e.106 ) e.107 = <F76 (e.105 ) (e.106 e.107 )> ;
(r3 e.105 ) () I e.107 = <F76 (e.105 ) (e.107 )> ;
(wm13 e.105 ) (I e.106 ) e.107 = <F41 (e.105 ) (e.106 ) e.107 I > ;
(wm13 e.105 ) () I e.107 = <F41 (e.105 ) () e.107 I > ;
(rp1-r15 ) (e.106 ) e.107 = True ;
(rp1-r15 r4 e.105 ) (I e.106 ) e.107 = <F101 (e.105 ) (e.106 e.107 )> ;
(rp1-r15 r4 e.105 ) () I e.107 = <F101 (e.105 ) (e.107 )> ;
(rp1-r15 r6 e.105 ) (e.106 ) e.107 = <F41 (e.105 ) (e.106 ) e.107 > ;
(rp1-r15 wh9 e.105 ) (e.106 ) e.107 = <F41 (e.105 ) (e.106 ) e.107 > ;
(rp1-r15 wm13 e.105 ) (I e.106 ) e.107 = <F41 (e.105 ) (e.106 ) e.107 I > ;
(rp1-r15 wm13 e.105 ) () I e.107 = <F41 (e.105 ) () e.107 I > ;
(rp1-r15 rp2-r19 e.105 ) (e.106 ) e.107 = <F5 (e.105 ) e.106 e.107 > ;
}
* InputFormat: <F76 (e.113 ) (e.114 ) e.115 >
F76 {
() (e.114 ) e.115 = True ;
(r5 e.113 ) (I e.114 ) e.115 = <F76 (e.113 ) (e.114 ) I e.115 > ;
(wm10 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(wm12 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(wm14 e.113 ) (I e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I I e.115 > ;
(rp1-r16 e.113 ) (e.114 ) e.115 = <F101 (e.113 ) (e.114 ) e.115 > ;
(rp1-r17 e.113 ) (e.114 ) e.115 = <F149 (e.113 ) (e.114 ) e.115 > ;
(repS-r21 e.113 ) (I e.114 ) e.115 = <F658 (e.113 ) () (e.114 ) I e.115 > ;
(repS-r22 e.113 ) (e.114 ) e.115 = <F658 (e.113 ) () (e.114 ) e.115 > ;
}
* InputFormat: <F101 (e.113 ) (e.114 ) e.115 >
F101 {
() (e.114 ) e.115 = True ;
(r5 e.113 ) (I e.114 ) e.115 = <F101 (e.113 ) (e.114 ) I e.115 > ;
(r7 e.113 ) (e.114 ) e.115 = <F76 (e.113 ) (e.114 ) e.115 > ;
(wm11 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(wm12 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(wm14 e.113 ) (I e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I I e.115 > ;
(rp1-r17 e.113 ) (e.114 ) e.115 = <F131 (e.113 ) (e.114 ) e.115 > ;
(rp2-r18 e.113 ) (e.114 ) e.115 = <F27 (e.113 ) (I e.114 ) e.115 > ;
(repS-r20 e.113 ) (e.114 ) e.115 = <F999 (e.113 ) (e.114 ) e.115 > ;
(repS-r21 e.113 ) (I e.114 ) e.115 = <F691 (e.113 ) () (e.114 ) I e.115 > ;
(repS-r22 e.113 ) (e.114 ) e.115 = <F691 (e.113 ) () (e.114 ) e.115 > ;
}
* InputFormat: <F131 (e.113 ) (e.114 ) e.115 >
F131 {
() (e.114 ) e.115 = True ;
(r5 e.113 ) (e.114 ) e.115 = <F101 (e.113 ) (e.114 ) e.115 > ;
(r7 e.113 ) (e.114 ) e.115 = <F149 (e.113 ) (e.114 ) e.115 > ;
(wm11 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (I e.114 ) e.115 > ;
(wm12 e.113 ) (e.114 ) I e.115 = <F41 (e.113 ) (I e.114 ) I e.115 > ;
(wm14 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(rp1-r17 e.113 ) (e.114 ) I e.115 = <F131 (e.113 ) (I e.114 ) e.115 > ;
(rp2-r18 e.113 ) (e.114 ) e.115 = <F956 (e.113 ) (e.114 ) e.115 > ;
(repS-r20 e.113 ) (e.114 ) e.115 = <F985 (e.113 ) (e.114 ) e.115 > ;
(repS-r21 e.113 ) (e.114 ) e.115 = <F691 (e.113 ) () (e.114 ) e.115 > ;
(repS-r22 e.113 ) (e.114 ) I e.115 = <F691 (e.113 ) () (I e.114 ) e.115 > ;
}
* InputFormat: <F985 (e.113 ) (e.114 ) e.115 >
F985 {
() (e.114 ) e.115 = False3 ;
(r5 e.113 ) (e.114 ) e.115 = <F999 (e.113 ) (e.114 ) e.115 > ;
(r6 e.113 ) (e.114 ) e.115 = <F1042 (e.113 ) (e.114 ) e.115 > ;
(wh9 e.113 ) (e.114 ) e.115 = <F1042 (e.113 ) (e.114 ) e.115 > ;
(wm12 e.113 ) (e.114 ) I e.115 = <F41 (e.113 ) (I e.114 ) I e.115 > ;
(wm14 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(rp1-r17 e.113 ) (e.114 ) I e.115 = <F985 (e.113 ) (I e.114 ) e.115 > ;
(rp2-r19 e.113 ) (e.114 ) e.115 = <F732 (e.113 ) () (e.114 ) e.115 > ;
(repS-r21 e.113 ) (e.114 ) e.115 = <F837 (e.113 ) () (e.114 ) e.115 > ;
(repS-r22 e.113 ) (e.114 ) I e.115 = <F837 (e.113 ) () (I e.114 ) e.115 > ;
}
* InputFormat: <F999 (e.113 ) (e.114 ) e.115 >
F999 {
() (I e.114 ) e.115 = False3 ;
() (e.114 ) e.115 = True ;
(r5 e.113 ) (I e.114 ) e.115 = <F999 (e.113 ) (e.114 ) I e.115 > ;
(r6 e.113 ) (e.114 ) e.115 = <F1018 (e.113 ) (e.114 ) e.115 > ;
(wh9 e.113 ) (e.114 ) e.115 = <F1018 (e.113 ) (e.114 ) e.115 > ;
(wm12 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(wm14 e.113 ) (I e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I I e.115 > ;
(rp1-r17 e.113 ) (e.114 ) e.115 = <F985 (e.113 ) (e.114 ) e.115 > ;
(rp2-r19 e.113 ) (e.114 ) e.115 = <F748 (e.113 ) () (e.114 ) e.115 > ;
(repS-r21 e.113 ) (I e.114 ) e.115 = <F837 (e.113 ) () (e.114 ) I e.115 > ;
(repS-r22 e.113 ) (e.114 ) e.115 = <F837 (e.113 ) () (e.114 ) e.115 > ;
}
* InputFormat: <F1018 (e.113 ) (e.114 ) e.115 >
F1018 {
() (e.114 ) e.115 = True ;
(r5 e.113 ) (I e.114 ) e.115 = <F1018 (e.113 ) (e.114 ) I e.115 > ;
(wm12 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(wm14 e.113 ) (I e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I I e.115 > ;
(rp1-r15 e.113 ) (e.114 ) e.115 = <F999 (e.113 ) (e.114 ) e.115 > ;
(rp1-r17 e.113 ) (e.114 ) e.115 = <F1042 (e.113 ) (e.114 ) e.115 > ;
(repS-r21 e.113 ) (I e.114 ) e.115 = <F861 (e.113 ) () (e.114 ) I e.115 > ;
(repS-r22 e.113 ) (e.114 ) e.115 = <F861 (e.113 ) () (e.114 ) e.115 > ;
}
* InputFormat: <F1042 (e.113 ) (e.114 ) e.115 >
F1042 {
() (e.114 ) e.115 = True ;
(r5 e.113 ) (e.114 ) e.115 = <F1018 (e.113 ) (e.114 ) e.115 > ;
(wm12 e.113 ) (e.114 ) I e.115 = <F41 (e.113 ) (I e.114 ) I e.115 > ;
(wm14 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(rp1-r15 e.113 ) (e.114 ) e.115 = <F985 (e.113 ) (e.114 ) e.115 > ;
(rp1-r17 e.113 ) (e.114 ) I e.115 = <F1042 (e.113 ) (I e.114 ) e.115 > ;
(repS-r21 e.113 ) (e.114 ) e.115 = <F861 (e.113 ) () (e.114 ) e.115 > ;
(repS-r22 e.113 ) (e.114 ) I e.115 = <F861 (e.113 ) () (I e.114 ) e.115 > ;
}
* InputFormat: <F956 (e.113 ) (e.114 ) e.115 >
F956 {
() (e.114 ) e.115 = True ;
(r5 e.113 ) (e.114 ) e.115 = <F27 (e.113 ) (I e.114 ) e.115 > ;
(wm12 e.113 ) (e.114 ) I e.115 = <F41 (e.113 ) (I I e.114 ) e.115 > ;
(wm14 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (I e.114 ) e.115 > ;
(rp1-r17 e.113 ) (e.114 ) I e.115 = <F956 (e.113 ) (I e.114 ) e.115 > ;
(repS-r21 e.113 ) (e.114 ) e.115 = <F732 (e.113 ) () (e.114 ) e.115 > ;
(repS-r22 e.113 ) (e.114 ) I e.115 = <F732 (e.113 ) () (I e.114 ) e.115 > ;
}
* InputFormat: <F149 (e.113 ) (e.114 ) e.115 >
F149 {
() (e.114 ) e.115 = True ;
(r5 e.113 ) (e.114 ) e.115 = <F76 (e.113 ) (e.114 ) e.115 > ;
(wm10 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (I e.114 ) e.115 > ;
(wm12 e.113 ) (e.114 ) I e.115 = <F41 (e.113 ) (I e.114 ) I e.115 > ;
(wm14 e.113 ) (e.114 ) e.115 = <F41 (e.113 ) (e.114 ) I e.115 > ;
(rp1-r16 e.113 ) (e.114 ) e.115 = <F131 (e.113 ) (e.114 ) e.115 > ;
(rp1-r17 e.113 ) (e.114 ) I e.115 = <F149 (e.113 ) (I e.114 ) e.115 > ;
(repS-r21 e.113 ) (e.114 ) e.115 = <F658 (e.113 ) () (e.114 ) e.115 > ;
(repS-r22 e.113 ) (e.114 ) I e.115 = <F658 (e.113 ) () (I e.114 ) e.115 > ;
}
* InputFormat: <F658 (e.260 ) (e.261 ) (e.262 ) e.263 >
F658 {
() (e.261 ) (e.262 ) e.263 = True ;
(r2 e.260 ) (e.261 ) (e.262 ) e.263 = <F76 (e.260 ) (e.262 e.261 ) e.263> ;
(r5 e.260 ) (e.261 ) (I e.262 ) e.263 = <F658 (e.260 ) (e.261 ) (e.262 ) I e.263 > ;
(wm10 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) e.263 > ;
(wm12 e.260 ) (e.261 ) (e.262 ) I e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(wm13 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (e.261 e.262 ) I e.263 > ;
(wm14 e.260 ) (e.261 ) (I e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(rp1-r16 e.260 ) (e.261 ) (e.262 ) e.263 = <F691 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(rp1-r17 e.260 ) (e.261 ) (e.262 ) I e.263 = <F658 (e.260 ) (e.261 ) (I e.262 ) e.263 > ;
(repS-r21 e.260 ) (e.261 ) (I e.262 ) e.263 = <F658 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
(repS-r22 e.260 ) (e.261 ) (e.262 ) I e.263 = <F658 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
}
* InputFormat: <F691 (e.260 ) (e.261 ) (e.262 ) e.263 >
F691 {
() (e.261 ) (e.262 ) e.263 = True ;
(r2 e.260 ) (e.261 ) (e.262 ) e.263 = <F101 (e.260 ) (e.262 e.261 ) e.263 > ;
(r5 e.260 ) (e.261 ) (I e.262 ) e.263 = <F691 (e.260 ) (e.261 ) (e.262 ) I e.263 > ;
(r7 e.260 ) (e.261 ) (e.262 ) e.263 = <F658 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(wm11 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) e.263 > ;
(wm12 e.260 ) (e.261 ) (e.262 ) I e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(wm13 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (e.261 e.262 ) I e.263 > ;
(wm14 e.260 ) (e.261 ) (I e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(rp1-r17 e.260 ) (e.261 ) (e.262 ) I e.263 = <F691 (e.260 ) (e.261 ) (I e.262 ) e.263 > ;
(rp2-r18 e.260 ) (e.261 ) (e.262 ) e.263 = <F732 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(repS-r20 e.260 ) (e.261 ) (e.262 ) e.263 = <F837 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(repS-r21 e.260 ) (e.261 ) (I e.262 ) e.263 = <F691 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
(repS-r22 e.260 ) (e.261 ) (e.262 ) I e.263 = <F691 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
}
* InputFormat: <F837 (e.260 ) (e.261 ) (e.262 ) e.263 >
F837 {
() (e.261 ) (I e.262 ) e.263 = False3 ;
() (e.261 ) (e.262 ) e.263 = True ;
(r4 e.260 ) (e.261 ) (e.262 ) e.263 = <F101 (e.260 ) (e.262 e.261 ) e.263 > ;
(r5 e.260 ) (e.261 ) (I e.262 ) e.263 = <F837 (e.260 ) (e.261 ) (e.262 ) I e.263 > ;
(r6 e.260 ) (e.261 ) (e.262 ) e.263 = <F861 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(wh9 e.260 ) (e.261 ) (e.262 ) e.263 = <F861 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(wm12 e.260 ) (e.261 ) (e.262 ) I e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(wm13 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (e.261 e.262 ) I e.263 > ;
(wm14 e.260 ) (e.261 ) (I e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(rp1-r17 e.260 ) (e.261 ) (e.262 ) I e.263 = <F837 (e.260 ) (e.261 ) (I e.262 ) e.263 > ;
(rp2-r19 e.260 ) (e.261 ) (e.262 ) e.263 = <F782 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(repS-r21 e.260 ) (e.261 ) (I e.262 ) e.263 = <F837 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
(repS-r22 e.260 ) (e.261 ) (e.262 ) I e.263 = <F837 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
}
* InputFormat: <F861 (e.260 ) (e.261 ) (e.262 ) e.263 >
F861 {
() (e.261 ) (e.262 ) e.263 = True ;
(r3 e.260 ) (e.261 ) (e.262 ) e.263 = <F76 (e.260 ) (e.262 e.261 ) e.263 > ;
(r5 e.260 ) (e.261 ) (I e.262 ) e.263 = <F861 (e.260 ) (e.261 ) (e.262 ) I e.263 > ;
(wm12 e.260 ) (e.261 ) (e.262 ) I e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(wm13 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (e.261 e.262 ) I e.263 > ;
(wm14 e.260 ) (e.261 ) (I e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(rp1-r15 e.260 ) (e.261 ) (e.262 ) e.263 = <F837 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(rp1-r17 e.260 ) (e.261 ) (e.262 ) I e.263 = <F861 (e.260 ) (e.261 ) (I e.262 ) e.263 > ;
(repS-r21 e.260 ) (e.261 ) (I e.262 ) e.263 = <F861 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
(repS-r22 e.260 ) (e.261 ) (e.262 ) I e.263 = <F861 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
}
* InputFormat: <F732 (e.260 ) (e.261 ) (e.262 ) e.263 >
F732 {
() (e.261 ) (e.262 ) e.263 = True ;
(r2 e.260 ) (e.261 ) (e.262 ) e.263 = <F27 (e.260 ) (I e.262 e.261 ) e.263 > ;
(r5 e.260 ) (e.261 ) (e.262 ) e.263 = <F748 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(wm12 e.260 ) (e.261 ) (e.262 ) I e.263 = <F41 (e.260 ) (I e.261 I e.262 ) e.263 > ;
(wm13 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (e.261 I e.262 ) e.263 > ;
(wm14 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) e.263 > ;
(rp1-r17 e.260 ) (e.261 ) (e.262 ) I e.263 = <F732 (e.260 ) (e.261 ) (I e.262 ) e.263 > ;
(repS-r21 e.260 ) (e.261 ) (e.262 ) e.263 = <F782 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(repS-r22 e.260 ) (e.261 ) (e.262 ) I e.263 = <F732 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
}
* InputFormat: <F748 (e.260 ) (e.261 ) (e.262 ) e.263 >
F748 {
() (e.261 ) (e.262 ) e.263 = True ;
(r2 e.260 ) (e.261 ) (e.262 ) e.263 = <F27 (e.260 ) (e.262 e.261 ) I e.263 > ;
(r5 e.260 ) (e.261 ) (I e.262 ) e.263 = <F748 (e.260 ) (e.261 ) (e.262 ) I e.263 > ;
(wm12 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) e.263 > ;
(wm13 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (e.261 e.262 ) I e.263 > ;
(wm14 e.260 ) (e.261 ) (I e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) I e.263 > ;
(rp1-r17 e.260 ) (e.261 ) (e.262 ) e.263 = <F732 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
(repS-r21 e.260 ) (e.261 ) (I e.262 ) e.263 = <F748 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
(repS-r22 e.260 ) (e.261 ) (e.262 ) e.263 = <F782 (e.260 ) (e.261 ) (e.262 ) e.263 > ;
}
* InputFormat: <F782 (e.260 ) (e.261 ) (e.262 ) e.263 >
F782 {
() (e.261 ) (e.262 ) e.263 = True ;
(r2 e.260 ) (e.261 ) (e.262 ) e.263 = <F27 (e.260 ) (e.262 I e.261 ) e.263 > ;
(r5 e.260 ) (e.261 ) (I e.262 ) e.263 = <F748 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
(wm12 e.260 ) (e.261 ) (e.262 ) I e.263 = <F41 (e.260 ) (I I e.261 e.262 ) e.263 > ;
(wm13 e.260 ) (e.261 ) (e.262 ) e.263 = <F41 (e.260 ) (I e.261 e.262 ) e.263 > ;
(wm14 e.260 ) (e.261 ) (I e.262 ) e.263 = <F41 (e.260 ) (I I e.261 e.262 ) e.263 > ;
(rp1-r17 e.260 ) (e.261 ) (e.262 ) I e.263 = <F732 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
(repS-r21 e.260 ) (e.261 ) (I e.262 ) e.263 = <F782 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
(repS-r22 e.260 ) (e.261 ) (e.262 ) I e.263 = <F782 (e.260 ) (I e.261 ) (e.262 ) e.263 > ;
}
****************************** The End ************************************
|
nemytykh@math.botik.ru
|