f0_12 sf -.927(Events)A 153 345 337 80 rC 168 419 :M f9_12 sf (a)S 153 345 337 79 rC 176 422 :M f4_7 sf (1)S 153 345 337 51 rC 406 390 :M f9_12 sf (b)S 153 345 337 50 rC 412 393 :M f4_7 sf (1)S gR gS 153 345 337 113 rC 407 452 :M f9_12 sf (b)S 153 345 337 112 rC 414 455 :M f4_7 sf (2)S gR gS 31 31 552 730 rC 250 485 :M f2_12 sf -.023(Figure 3.3:)A 322 485 :M -.01(Fork Module)A 97 515 :M .621 .062(The Fork Module, upon receiving an input event, generates an output event on)J 97 533 :M .155 .015(both of two separate streams. Either ordering of output events is allowed by the)J 97 551 :M 1.993 .199(grammar. Like the Basic Module, input events may queue up before their)J 97 569 :M -.002(corresponding output events are generated.)A 237 587 28 12 rC 265 599 :M psb currentpoint pse 237 587 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (m) -4 261 sh 384 /Symbol f1 (=) 372 261 sh 384 /Times-Roman f1 (1) 648 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 265 601 :M f2_12 sf ( )S 268 587 28 12 rC 296 599 :M psb currentpoint pse 268 587 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (n) -8 261 sh 384 /Symbol f1 (=) 280 261 sh 384 /Times-Roman f1 (2) 587 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 296 601 :M f2_12 sf ( )S 299 587 26 12 rC 325 599 :M psb currentpoint pse 299 587 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 832 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (b) -9 261 sh 384 /Symbol f1 (=) 281 261 sh 384 /Times-Roman f1 (1) 557 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 325 601 :M f2_12 sf ( )S 328 585 41 18 rC 369 603 :M psb currentpoint pse 328 585 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1312 div 576 3 -1 roll exch div scale currentpoint translate 64 56 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (S) -3 328 sh (s) 761 328 sh 384 /Symbol f1 (=) 290 328 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1401 /Symbol f3 ({) 586 361 sh (}) 1043 361 sh 224 /Times-Roman f1 (0) 906 424 sh end MTsave restore pse gR gS 31 31 552 730 rC 369 601 :M f2_12 sf ( )S 372 587 34 12 rC 406 599 :M psb currentpoint pse 372 587 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1088 div 384 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (N) 13 276 sh 384 /Symbol f1 (=) 389 276 sh (\306) 693 276 sh end MTsave restore pse gR gS 153 616 138 19 rC 291 635 :M psb currentpoint pse 153 616 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4416 div 608 3 -1 roll exch div scale currentpoint translate 64 59 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -83 227 1924 31 vb 16 th 83 227 1841 258 vb 16 th 83 227 2805 31 vb 16 th -83 227 2888 258 vb 16 th -83 227 3133 31 vb 16 th 83 227 3050 258 vb 16 th 83 227 4050 31 vb 16 th -83 227 4133 258 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (prereq) 28 357 sh 224 ns (s) 1050 453 sh 160 /Times-Roman f1 (0) 1132 509 sh 224 ns (1) 2191 453 sh (1) 2656 453 sh (1) 3400 453 sh (2) 3883 453 sh 384 /Symbol f1 (=) 1364 357 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1578 /Symbol f3 ({) 1660 407 sh (}) 4148 407 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 1939 357 sh (b) 2452 357 sh (a) 3148 357 sh (b) 3661 357 sh 384 /Times-Roman f1 (,) 2316 357 sh (,) 2909 357 sh (,) 3525 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 291 633 :M f2_12 sf ( )S 294 618 51 17 rC 345 635 :M psb currentpoint pse 294 618 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1632 div 544 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (r) -9 292 sh 224 ns (s) 100 388 sh 160 /Times-Roman f1 (0) 182 444 sh 384 ns (0) 833 292 sh 384 /Symbol f1 (=) 414 292 sh (\245) 1152 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) 699 315 sh (]) 1433 315 sh 384 /Times-Roman f1 (,) 1020 292 sh end MTsave restore pse gR gS 31 31 552 730 rC 345 633 :M f2_12 sf ( )S 348 616 142 20 rC 490 636 :M psb currentpoint pse 348 616 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4544 div 640 3 -1 roll exch div scale currentpoint translate 64 33 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPT) 10 383 sh (T) 1436 383 sh (Y) 2535 383 sh (Z) 3082 383 sh (Z) 3670 383 sh 224 ns (s) 657 479 sh (s) 1771 479 sh (s) 2869 479 sh (s) 3457 479 sh (s) 4081 479 sh 160 /Times-Roman f1 (0) 739 535 sh (0) 1853 535 sh (0) 2951 535 sh (0) 3539 535 sh (0) 4163 535 sh 224 ns (1) 1594 479 sh (1) 2692 479 sh (1) 3280 479 sh (2) 3886 479 sh 384 /Symbol f1 (=) 971 383 sh (\256) 2071 383 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1736 /Symbol f3 ({) 1267 448 sh (}) 4286 448 sh 224 /Times-Roman f1 (,) 1697 479 sh (,) 2795 479 sh (,) 3383 479 sh (,) 4007 479 sh end MTsave restore pse gR gS 31 31 552 730 rC 97 663 :M f2_12 sf .162 .016(The basic productions for the Fork Module generate a language whose sentences)J 97 681 :M .32 .032(are series of zero or more complete transactions made up of a single input event)J 97 699 :M 1.18 .118(followed by each of the two output events. In specification of the transaction)J endp %%Page: 99 99 %%BeginPageSetup initializepage (nestor; page: 99 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(48)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 64 100 :M f2_12 sf -.02(The derived values from the specification are:)A 259 116 59 17 rC 318 133 :M psb currentpoint pse 259 116 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1888 div 544 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (E) 6 325 sh 384 /Symbol f1 (=) 347 325 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1382 /Symbol f3 ({) 643 356 sh (}) 1630 356 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 794 325 sh (b) 1307 325 sh 224 /Times-Roman f1 (1) 1046 421 sh (1) 1511 421 sh 384 /Times-Roman f1 (,) 1171 325 sh end MTsave restore pse gR gS 204 148 68 17 rC 272 165 :M psb currentpoint pse 204 148 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2176 div 544 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-BoldItalic f1 (V) -18 292 sh (A) 851 292 sh 384 /Symbol f1 (=) 355 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1182 /Symbol f3 ({) 651 305 sh (}) 1081 305 sh 384 /Symbol f1 (\310) 1322 292 sh 384 /Times-Italic f1 (V) 1683 292 sh 224 ns (s) 1884 388 sh 160 /Times-Roman f1 (0) 1966 444 sh end MTsave restore pse gR gS 31 31 552 730 rC 272 163 :M f2_12 sf ( )S 275 146 99 20 rC 374 166 :M psb currentpoint pse 275 146 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3168 div 640 3 -1 roll exch div scale currentpoint translate 64 33 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-BoldItalic f1 (P) 10 383 sh (A) 847 383 sh 384 /Symbol f1 (=) 351 383 sh (\256) 1172 383 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1736 /Symbol f3 ({) 647 448 sh (}) 2085 448 sh 384 /Symbol f1 (\310) 2326 383 sh 384 /Times-Italic f1 (A) 1669 383 sh (P) 2709 383 sh 224 ns (s) 1880 479 sh (s) 2880 479 sh 160 /Times-Roman f1 (0) 1962 535 sh (0) 2962 535 sh end MTsave restore pse gR gS 118 186 160 20 rC 278 206 :M psb currentpoint pse 118 186 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 5120 div 640 3 -1 roll exch div scale currentpoint translate 64 33 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (V) -16 383 sh (A) 993 383 sh (B) 1566 383 sh (T) 2273 383 sh (Y) 3574 383 sh (Z) 4267 383 sh 224 ns (s) 185 479 sh (s) 1204 479 sh (s) 1933 479 sh (s) 2608 479 sh (s) 3908 479 sh (s) 4642 479 sh 160 /Times-Roman f1 (0) 267 535 sh (0) 1286 535 sh (0) 2015 535 sh (0) 2690 535 sh (0) 3990 535 sh (0) 4724 535 sh 224 ns (1) 1756 479 sh (1) 2431 479 sh (1) 3731 479 sh (1) 4465 479 sh 384 /Symbol f1 (=) 499 383 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1736 /Symbol f3 ({) 795 448 sh (}) 2813 448 sh 384 /Symbol f1 (\310) 3054 383 sh 384 1000 1736 /Symbol f3 ({) 3409 448 sh (}) 4847 448 sh 384 /Times-Roman f1 (,) 1415 383 sh (,) 2144 383 sh (,) 4119 383 sh 224 ns (,) 1859 479 sh (,) 2534 479 sh (,) 3834 479 sh (,) 4568 479 sh end MTsave restore pse gR gS 31 31 552 730 rC 278 203 :M f2_12 sf ( )S 281 179 178 34 rC 459 213 :M psb currentpoint pse 281 179 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 5696 div 1088 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPA) 10 596 sh (A) 1497 596 sh (B) 2498 596 sh (Y) 3928 294 sh (Z) 3887 808 sh 224 ns (s) 689 692 sh (s) 1708 692 sh (s) 2865 692 sh (s) 4262 390 sh (s) 4262 904 sh 160 /Times-Roman f1 (0) 771 748 sh (0) 1790 748 sh (0) 2947 748 sh (0) 4344 446 sh (0) 4344 960 sh 224 ns (1) 2688 692 sh (1) 4085 390 sh (1) 5264 390 sh (1) 4085 904 sh (1) 5241 904 sh 384 /Symbol f1 (=) 1003 596 sh (\256) 2008 596 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1736 /Symbol f3 ({) 1299 661 sh (}) 3070 661 sh 384 /Symbol f1 (\310) 3311 596 sh (\256) 4562 294 sh (\256) 4562 808 sh (\354) 3683 355 sh (\355) 3683 661 sh (\356) 3683 968 sh (\374) 5407 355 sh (\375) 5407 661 sh (\376) 5407 968 sh 224 /Times-Roman f1 (,) 2791 692 sh (,) 4188 390 sh (,) 4188 904 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 5012 294 sh (b) 5037 808 sh end MTsave restore pse gR gS 132 226 128 34 rC 260 260 :M psb currentpoint pse 132 226 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4096 div 1088 3 -1 roll exch div scale currentpoint translate 64 56 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPB) 10 584 sh (B) 1523 293 sh (T) 2658 293 sh (B) 3209 293 sh (B) 1523 784 sh 224 ns (s) 689 680 sh (s) 1890 389 sh (s) 2993 389 sh (s) 3576 389 sh (s) 1890 880 sh 160 /Times-Roman f1 (0) 771 736 sh (0) 1972 445 sh (0) 3075 445 sh (0) 3658 445 sh (0) 1972 936 sh 224 ns (1) 1713 389 sh (1) 2816 389 sh (1) 3399 389 sh (1) 1713 880 sh 384 /Symbol f1 (=) 1003 584 sh (\256) 2190 293 sh (\256) 2190 784 sh (\354) 1316 355 sh (\355) 1316 649 sh (\356) 1316 944 sh (\374) 3805 355 sh (\375) 3805 649 sh (\376) 3805 944 sh 224 /Times-Roman f1 (,) 1816 389 sh (,) 2919 389 sh (,) 3502 389 sh (,) 1816 880 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (e) 2654 784 sh end MTsave restore pse gR gS 31 31 552 730 rC 260 250 :M f2_12 sf ( )S 263 233 135 20 rC 398 253 :M psb currentpoint pse 263 233 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4320 div 640 3 -1 roll exch div scale currentpoint translate 64 33 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (DP) 10 383 sh (Z) 1256 383 sh (Y) 1821 383 sh (Y) 2919 383 sh (Z) 3466 383 sh 224 ns (s) 458 479 sh (s) 1631 479 sh (s) 2155 479 sh (s) 3253 479 sh (s) 3841 479 sh 160 /Times-Roman f1 (0) 540 535 sh (0) 1713 535 sh (0) 2237 535 sh (0) 3335 535 sh (0) 3923 535 sh 224 ns (1) 1454 479 sh (1) 1978 479 sh (1) 3076 479 sh (1) 3664 479 sh 384 /Symbol f1 (=) 772 383 sh (\256) 2455 383 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1736 /Symbol f3 ({) 1068 448 sh (}) 4046 448 sh 224 /Times-Roman f1 (,) 1557 479 sh (,) 2081 479 sh (,) 3179 479 sh (,) 3767 479 sh end MTsave restore pse gR gS 31 31 552 730 rC 398 250 :M f2_12 sf ( )S 401 236 43 16 rC 444 252 :M psb currentpoint pse 401 236 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1376 div 512 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (SP) -3 276 sh 224 ns (s) 360 372 sh 160 /Times-Roman f1 (0) 442 428 sh 384 /Symbol f1 (=) 674 276 sh (\306) 978 276 sh end MTsave restore pse gR gS 31 31 552 730 rC 64 287 :M f2_12 sf .185 .019(The module is defined to have a single input, a single output, and a single block.)J 64 305 :M .637 .064(In addition, only a single state is defined\321the next state relation is undefined,)J 64 323 :M -.006(so the module stays in its initial state throughout its operation.)A 64 353 :M 4.068 .407(The basic productions generate sequences with zero or more complete)J 64 370 :M .285 .028(transactions, in which input events \(denoted by )J 334 360 14 14 rC 348 374 :M psb currentpoint pse 334 360 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 448 div 448 3 -1 roll exch div scale currentpoint translate 64 59 translate -15 261 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) show 236 357 moveto 224 /Times-Roman f1 (1) show end pse gR gS 31 31 552 730 rC 348 370 :M f2_12 sf .208 .021(\) are immediately followed by)J 64 388 :M 1.775 .177(their corresponding output event \(denoted by )J 336 378 12 14 rC 348 392 :M psb currentpoint pse 336 378 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 448 3 -1 roll exch div scale currentpoint translate 64 36 translate -23 284 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) show 189 380 moveto 224 /Times-Roman f1 (1) show end pse gR gS 31 31 552 730 rC 348 388 :M f2_12 sf 1.781 .178(\). The prerequisite relation)J 64 406 :M -.025(reflects the dependence of )A 211 396 12 14 rC 223 410 :M psb currentpoint pse 211 396 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 448 3 -1 roll exch div scale currentpoint translate 64 36 translate -23 284 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) show 189 380 moveto 224 /Times-Roman f1 (1) show end pse gR gS 31 31 552 730 rC 223 406 :M f2_12 sf -.033( events on )A 282 396 14 14 rC 296 410 :M psb currentpoint pse 282 396 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 448 div 448 3 -1 roll exch div scale currentpoint translate 64 59 translate -15 261 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) show 236 357 moveto 224 /Times-Roman f1 (1) show end pse gR gS 31 31 552 730 rC 296 406 :M f2_12 sf -.095( events.)A 64 437 :M 2.594 .259(The following event sequences are examples of sentences in the language)J 64 452 :M -.006(generated by the basic production set )A 274 442 22 16 rC 296 458 :M psb currentpoint pse 274 442 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 704 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 261 sh 224 ns (s) 415 357 sh 160 /Times-Roman f1 (0) 497 413 sh end MTsave restore pse gR gS 31 31 552 730 rC 296 452 :M f2_12 sf -.086(:)A f2_9 sf 0 -3 rm -.259(49)A 0 3 rm 236 471 106 51 rC 342 522 :M psb currentpoint pse 236 471 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3392 div 1632 3 -1 roll exch div scale currentpoint translate 64 -7 translate 1548 261 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (e) show 1315 668 moveto (a) show 1566 764 moveto 224 /Times-Roman f1 (1) show 1663 668 moveto 384 /Symbol f2 (b) show 1875 764 moveto 224 /Times-Roman f1 (1) show 650 1088 moveto 384 /Symbol f2 (a) show 901 1184 moveto 224 /Times-Roman f1 (1) show 998 1088 moveto 384 /Symbol f2 (b) show 1210 1184 moveto 224 /Times-Roman f1 (1) show 1315 1088 moveto 384 /Symbol f2 (a) show 1566 1184 moveto 224 /Times-Roman f1 (1) show 1663 1088 moveto 384 /Symbol f2 (b) show 1875 1184 moveto 224 /Times-Roman f1 (1) show 1980 1088 moveto 384 /Symbol f2 (a) show 2231 1184 moveto 224 /Times-Roman f1 (1) show 2328 1088 moveto 384 /Symbol f2 (b) show 2540 1184 moveto 224 /Times-Roman f1 (1) show -15 1508 moveto 384 /Symbol f2 (a) show 236 1604 moveto 224 /Times-Roman f1 (1) show 333 1508 moveto 384 /Symbol f2 (b) show 545 1604 moveto 224 /Times-Roman f1 (1) show 650 1508 moveto 384 /Symbol f2 (a) show 901 1604 moveto 224 /Times-Roman f1 (1) show 998 1508 moveto 384 /Symbol f2 (b) show 1210 1604 moveto 224 /Times-Roman f1 (1) show 1315 1508 moveto 384 /Symbol f2 (a) show 1566 1604 moveto 224 /Times-Roman f1 (1) show 1663 1508 moveto 384 /Symbol f2 (b) show 1875 1604 moveto 224 /Times-Roman f1 (1) show 1980 1508 moveto 384 /Symbol f2 (a) show 2231 1604 moveto 224 /Times-Roman f1 (1) show 2328 1508 moveto 384 /Symbol f2 (b) show 2540 1604 moveto 224 /Times-Roman f1 (1) show 2645 1508 moveto 384 /Symbol f2 (a) show 2896 1604 moveto 224 /Times-Roman f1 (1) show 2993 1508 moveto 384 /Symbol f2 (b) show 3205 1604 moveto 224 /Times-Roman f1 (1) show end pse gR gS 31 31 552 730 rC 64 549 :M f2_12 sf 1.118 .112(Next we consider the delay productions. Because of the possibility)J 452 546 :M f2_9 sf .257(50)A f2_12 sf 0 3 rm .88 .088( that the)J 0 -3 rm 64 567 :M 1.478 .148(output event corresponding to a particular input event may be delayed until)J 64 585 :M .472 .047(after an arbitrary number of new input events have occurred, a new production)J 64 603 :M 2.357 .236(must be introduced. In effect, the \(context-sensitive\) delay production set)J 64 607 135 20 rC 199 627 :M psb currentpoint pse 64 607 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4320 div 640 3 -1 roll exch div scale currentpoint translate 64 33 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (DP) 10 383 sh (Z) 1256 383 sh (Y) 1821 383 sh (Y) 2919 383 sh (Z) 3466 383 sh 224 ns (s) 458 479 sh (s) 1631 479 sh (s) 2155 479 sh (s) 3253 479 sh (s) 3841 479 sh 160 /Times-Roman f1 (0) 540 535 sh (0) 1713 535 sh (0) 2237 535 sh (0) 3335 535 sh (0) 3923 535 sh 224 ns (1) 1454 479 sh (1) 1978 479 sh (1) 3076 479 sh (1) 3664 479 sh 384 /Symbol f1 (=) 772 383 sh (\256) 2455 383 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1736 /Symbol f3 ({) 1068 448 sh (}) 4046 448 sh 224 /Times-Roman f1 (,) 1557 479 sh (,) 2081 479 sh (,) 3179 479 sh (,) 3767 479 sh end MTsave restore pse gR gS 31 31 552 730 rC 199 620 :M f2_12 sf 1.224 .122( allows output events to \322percolate\323 past the following)J 64 642 :M -.007(input events. This makes sequences like the following possible:)A -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 64 658.24 -.24 .24 207.24 658 .24 64 658 @a 64 675 :M f2_9 sf (49)S f2_10 sf 0 3 rm -.014(They are sentences generated by the grammar )A 0 -3 rm 292 665 103 20 rC 395 685 :M psb currentpoint pse 292 665 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3296 div 640 3 -1 roll exch div scale currentpoint translate 64 32 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -95 285 888 0 vb 16 th 95 285 793 285 vb 16 th 95 285 3085 0 vb 16 th -95 285 3180 285 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (\242) 280 390 sh (=) 475 384 sh 384 /Times-Italic f1 (G) -11 384 sh (V) 917 384 sh (E) 1476 384 sh (BP) 1865 384 sh (A) 2639 384 sh 224 ns (s) 1118 480 sh (s) 2270 480 sh (s) 2850 480 sh 160 /Times-Roman f1 (0) 1200 536 sh (0) 2352 536 sh (0) 2932 536 sh 384 /Times-Roman f1 (,) 1329 384 sh (,) 1714 384 sh (,) 2481 384 sh end MTsave restore pse gR gS 31 31 552 730 rC 395 678 :M f2_10 sf (.)S 64 693 :M f2_9 sf (50)S f2_10 sf 0 3 rm -.015(If we wish to remove this possibility, we set )A 0 -3 rm 278 686 46 16 rC 324 702 :M psb currentpoint pse 278 686 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1472 div 512 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (DP) 10 276 sh 224 ns (s) 458 372 sh 160 /Times-Roman f1 (0) 540 428 sh 384 /Symbol f1 (=) 772 276 sh (\306) 1076 276 sh end MTsave restore pse gR gS 31 31 552 730 rC 324 696 :M f2_10 sf (.)S endp %%Page: 100 100 %%BeginPageSetup initializepage (nestor; page: 100 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 97 64 :M f1_10 sf -.018(Modular Specification)A 533 64 :M f0_12 sf -.781(47)A 97 101 :M f0_13 sf -.155(3.4.1)A 142 101 :M -.058(Basic Module)A 166 116 312 110 rC 259 118 -2 2 387 170 2 259 116 @a -2 -2 261 226 2 2 385 170 @b -2 -2 261 226 2 2 259 116 @b 169 171 -1 1 248 170 1 169 170 @a np 247 170 :M 247 175 :L 259 170 :L 247 165 :L 247 170 :L eofill 387 172 -1 1 466 171 1 387 171 @a np 465 171 :M 465 176 :L 477 171 :L 465 166 :L 465 171 :L eofill 171 159 :M f0_12 sf -.495(Input Stream)A 185 186 :M f11_12 sf -.365( )A f0_12 sf -.927(Events)A 383 159 :M -.685(Output Stream)A 403 185 :M f11_12 sf -.365( )A f0_12 sf -.927(Events)A 268 174 :M -.606(Basic Module)A 166 116 312 75 rC 182 185 :M f9_12 sf (a)S 166 116 312 74 rC 190 188 :M f4_7 sf (1)S gR gS 166 116 312 76 rC 401 186 :M f9_12 sf (b)S 166 116 312 75 rC 407 189 :M f4_7 sf (1)S gR gS 31 31 552 730 rC 248 248 :M f2_12 sf -.023(Figure 3.2:)A 320 248 :M -.06(Basic Module)A 97 278 :M .195 .019(The Basic Module structure represents one of the simplest elements available in)J 97 295 :M 1.125 .113(the abstract representational structure. A single input event, )J 461 285 14 14 rC 475 299 :M psb currentpoint pse 461 285 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 448 div 448 3 -1 roll exch div scale currentpoint translate 64 59 translate -15 261 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) show 236 357 moveto 224 /Times-Roman f1 (1) show end pse gR gS 31 31 552 730 rC 475 295 :M f2_12 sf 1.044 .104(, triggers its)J 97 313 :M .101 .01(operation. After a possible processing delay, a corresponding output event, )J 518 303 12 14 rC 530 317 :M psb currentpoint pse 518 303 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 448 3 -1 roll exch div scale currentpoint translate 64 36 translate -23 284 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) show 189 380 moveto 224 /Times-Roman f1 (1) show end pse gR gS 31 31 552 730 rC 530 313 :M f2_12 sf (, is)S 97 332 :M .491 .049(generated. This delay may be a function of the specific input event provided as)J 97 350 :M 1.663 .166(input to the module. The existence of such a delay will only be visible if it)J 97 368 :M .604 .06(results in a reordering due to delay productions.)J 372 365 :M f2_9 sf .233(48)A f2_12 sf 0 3 rm .656 .066( As a result, it is possible to)J 0 -3 rm 97 386 :M 1.711 .171(queue input events in a Basic Module, while awaiting the occurrence of the)J 97 404 :M .197 .02(corresponding output. Section\3123.5.2 will provide an example demonstrating how)J 97 422 :M -.014(such queuing can be limited if an input buffer size restriction exists.)A 97 452 :M .35 .035(Because of its general nature, a Basic Module may easily be used to represent a)J 97 470 :M 1.223 .122(wide variety of real processing elements. For example, an input event might)J 97 488 :M 2.082 .208(represent the triggering of the start of a mathematical calculation, and an)J 97 506 :M .917 .092(output event indicates that the operation had completed. The following is the)J 97 524 :M -.002(modular specification of the Basic Module:)A 238 542 28 12 rC 266 554 :M psb currentpoint pse 238 542 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (m) -4 261 sh 384 /Symbol f1 (=) 372 261 sh 384 /Times-Roman f1 (1) 648 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 266 556 :M f2_12 sf ( )S 269 542 26 12 rC 295 554 :M psb currentpoint pse 269 542 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 832 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (n) -8 261 sh 384 /Symbol f1 (=) 280 261 sh 384 /Times-Roman f1 (1) 556 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 295 556 :M f2_12 sf ( )S 298 542 26 12 rC 324 554 :M psb currentpoint pse 298 542 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 832 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (b) -9 261 sh 384 /Symbol f1 (=) 281 261 sh 384 /Times-Roman f1 (1) 557 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 324 556 :M f2_12 sf ( )S 327 540 41 18 rC 368 558 :M psb currentpoint pse 327 540 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1312 div 576 3 -1 roll exch div scale currentpoint translate 64 56 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (S) -3 328 sh (s) 761 328 sh 384 /Symbol f1 (=) 290 328 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1401 /Symbol f3 ({) 586 361 sh (}) 1043 361 sh 224 /Times-Roman f1 (0) 906 424 sh end MTsave restore pse gR gS 31 31 552 730 rC 368 556 :M f2_12 sf ( )S 371 542 34 12 rC 405 554 :M psb currentpoint pse 371 542 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1088 div 384 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (N) 13 276 sh 384 /Symbol f1 (=) 389 276 sh (\306) 693 276 sh end MTsave restore pse gR gS 182 571 99 19 rC 281 590 :M psb currentpoint pse 182 571 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3168 div 608 3 -1 roll exch div scale currentpoint translate 64 59 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -83 227 1924 31 vb 16 th 83 227 1841 258 vb 16 th 83 227 2805 31 vb 16 th -83 227 2888 258 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (prereq) 28 357 sh 224 ns (s) 1050 453 sh 160 /Times-Roman f1 (0) 1132 509 sh 224 ns (1) 2191 453 sh (1) 2656 453 sh 384 /Symbol f1 (=) 1364 357 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1578 /Symbol f3 ({) 1660 407 sh (}) 2903 407 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 1939 357 sh (b) 2452 357 sh 384 /Times-Roman f1 (,) 2316 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 281 588 :M f2_12 sf ( )S 284 573 51 17 rC 335 590 :M psb currentpoint pse 284 573 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1632 div 544 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (r) -9 292 sh 224 ns (s) 100 388 sh 160 /Times-Roman f1 (0) 182 444 sh 384 ns (0) 833 292 sh 384 /Symbol f1 (=) 414 292 sh (\245) 1152 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) 699 315 sh (]) 1433 315 sh 384 /Times-Roman f1 (,) 1020 292 sh end MTsave restore pse gR gS 31 31 552 730 rC 335 591 :M f2_12 sf ( )S 338 571 123 20 rC 461 591 :M psb currentpoint pse 338 571 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3936 div 640 3 -1 roll exch div scale currentpoint translate 64 33 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPT) 10 383 sh (T) 1436 383 sh (Y) 2535 383 sh (Z) 3082 383 sh 224 ns (s) 657 479 sh (s) 1771 479 sh (s) 2869 479 sh (s) 3457 479 sh 160 /Times-Roman f1 (0) 739 535 sh (0) 1853 535 sh (0) 2951 535 sh (0) 3539 535 sh 224 ns (1) 1594 479 sh (1) 2692 479 sh (1) 3280 479 sh 384 /Symbol f1 (=) 971 383 sh (\256) 2071 383 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1736 /Symbol f3 ({) 1267 448 sh (}) 3662 448 sh 224 /Times-Roman f1 (,) 1697 479 sh (,) 2795 479 sh (,) 3383 479 sh end MTsave restore pse gR gS 31 31 552 730 rC -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 97 671.24 -.24 .24 240.24 671 .24 97 671 @a 97 684 :M f2_9 sf (48)S f2_10 sf 0 3 rm .018 .002(This is an artifact of the relativistic timing nature of the event system representation, as noted)J 0 -3 rm 97 699 :M -.034(in Section\3121.4.)A endp %%Page: 101 101 %%BeginPageSetup initializepage (nestor; page: 101 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(46)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 82 101 :M f2_12 sf .562 .056(recursive productions admit sentential forms like )J 366 91 53 12 rC 366 103 :M f3_12 sf -.436( )A 419 103 :M psb currentpoint pse 366 91 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1696 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (AAA) 17 261 sh (AA) 1144 261 sh 384 /MT-Extra f1 (K) 722 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 419 101 :M f2_12 sf .675 .068(. Because of the)J 82 119 :M .413 .041(form of the other productions, a lookahead of one symbol is always sufficient)J 82 137 :M -.029(to identify the last )A 188 127 11 11 rC 199 138 :M psb currentpoint pse 188 127 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 352 div 352 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (A) 17 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 199 137 :M f2_12 sf -.02( in one of these sentential forms.)A 64 166 :M .069 .007(These are consistent with )J 210 155 29 15 rC 239 170 :M psb currentpoint pse 210 155 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 928 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (LR) 12 292 sh 384 /Times-Roman f1 (1) 553 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1171 /Symbol f3 (\() 451 302 sh (\)) 722 302 sh end MTsave restore pse gR gS 31 31 552 730 rC 239 166 :M f2_12 sf .101 .01(, because the lookahead that may be necessary to)J 64 185 :M .536 .054(determine the required next move of the automaton in a parse is limited to one)J 64 203 :M .003 0(symbol. Because the terminals appear in a unique position, there will never be a)J 64 221 :M -.012(need to look ahead more than one symbol.)A 64 251 :M 1.374 .137(The \(context-sensitive\) shuffle and delay productions have a common form of)J 64 260 49 11 rC 113 271 :M psb currentpoint pse 64 260 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1568 div 352 3 -1 roll exch div scale currentpoint translate 64 27 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (ZY) 7 261 sh (YZ) 1008 261 sh 384 /Symbol f1 (\256) 544 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 113 269 :M f2_12 sf 1.513 .151(. They allow an event non-terminal symbol to interchange its place)J 64 287 :M .69 .069(with a following event non-terminal symbol. The D2SM of Turnbull, described)J 64 305 :M .355 .035(in Section\3122.4.1, is ideally constructed to shift the input text for such cases from)J 64 323 :M .816 .082(the right stack, into the left stack until the matching token is found, and then)J 64 341 :M -.004(shift the text back to the right stack. Hence, a parser for our module grammar is)A 64 359 :M .756 .076(a D2SM. Turnbull proves that a DRP grammar corresponds to each D2SM, so)J 64 377 :M .277 .028(the connection between Turnbull\325s DRP grammars and our module grammars is)J 64 395 :M -.011(easy and straightforward to make.)A 64 423 :M .962 .096(Finally, Turnbull showed that most questions that are decidable for )J 460 412 31 16 rC 491 428 :M psb currentpoint pse 460 412 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 992 div 512 3 -1 roll exch div scale currentpoint translate 64 58 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (LR) 12 294 sh (k) 589 294 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1182 /Symbol f3 (\() 451 305 sh (\)) 783 305 sh end MTsave restore pse gR gS 31 31 552 730 rC 491 423 :M f2_12 sf .512 .051( are)J 64 443 :M -.018(also decidable for DRP. Thus, it is always possible to construct a practical parser)A 64 461 :M 1.392 .139(that will be able to verify whether an event sequence is valid for the system)J 64 479 :M -.065(being modelled.)A 64 512 :M f0_14 sf -.484(3.4)A 109 512 :M -.201(S)A f0_12 sf -.185(INGLE)A f0_14 sf -.301(-S)A 175 512 :M f0_12 sf -.247(TATE )A 214 512 :M f0_14 sf (M)S 228 512 :M f0_12 sf -.114(ODULE )A f0_14 sf (E)S 290 512 :M f0_12 sf -.071(XAMPLES)A 64 543 :M f2_12 sf .03 .003(This section will take the general representation framework described above and)J 64 561 :M 1.613 .161(instantiate it for a number of particular single-state module examples. The)J 64 579 :M .94 .094(examples are not exhaustive, but are presented to demonstrate the breadth of)J 64 597 :M -.003(processing elements that can be represented under this framework.)A endp %%Page: 102 102 %%BeginPageSetup initializepage (nestor; page: 102 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 97 64 :M f1_10 sf -.018(Modular Specification)A 533 64 :M f0_12 sf -.781(45)A 97 91 174 25 rC 97 116 :M f3_12 sf -.436( )A 271 116 :M psb currentpoint pse 97 91 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 5568 div 800 3 -1 roll exch div scale currentpoint translate 64 38 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -77 194 77 53 vb 16 th 77 194 0 247 vb 16 th 77 194 1807 53 vb 16 th -77 194 1884 247 vb 16 th -84 230 2854 17 vb 16 th 84 230 2770 247 vb 16 th 84 230 5369 17 vb 16 th -84 230 5453 247 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (m) 118 346 sh (n) 524 346 sh (b) 841 346 sh (S) 1166 346 sh (N) 1510 346 sh (prereq) 2927 346 sh (r) 4200 346 sh (BPT) 4579 346 sh 224 ns (s) 3949 442 sh (s) 4309 442 sh (s) 5226 442 sh (s) 2355 718 sh (S) 2602 718 sh 384 /Times-Roman f1 (,) 391 346 sh (,) 709 346 sh (,) 1028 346 sh (,) 1356 346 sh (,) 4068 346 sh (,) 4428 346 sh 384 /Symbol f1 (\310) 1981 346 sh 224 ns (\316) 2459 718 sh 576 /MT-Extra f1 (U) 2345 433 sh end MTsave restore pse gR gS 31 31 552 730 rC 271 103 :M f2_12 sf 3.78 .378(. Thus, by specifying the values for these)J 97 131 :M -.007(parameters, we fully describe the module under the representation.)A 97 161 :M .131 .013(In the descriptions of the languages describing valid event \(execution\) sequences)J 97 179 :M .294 .029(that follow, only those sequences that are made up of complete transactions will)J 97 197 :M .399 .04(be generated by the grammars. In reality, the sets of valid event sequences are)J 97 215 :M .184 .018(all )J f1_12 sf .455 .046(prefix closed)J 185 215 :M f2_12 sf .526 .053(\321any prefix of such a valid event sequence is also a valid event)J 97 233 :M .629 .063(sequence. That is, if a particular event sequence is a valid one for a particular)J 97 251 :M .627 .063(module, then all prefixes of that string \(formed by removing one or more of the)J 97 269 :M 3.338 .334(\322tail\323 events\) are also valid sequences. For simplicity, such incomplete)J 97 287 :M -.002(sequences are not explicit members of the language representations.)A 97 320 :M f0_14 sf -.484(3.3)A 142 320 :M (D)S 154 320 :M f0_12 sf -.042(ECIDABILITY )A f0_14 sf (I)S f0_12 sf -.047(SSUES FOR )A 331 320 :M f0_14 sf -.316(M)A f0_12 sf -.234(ODULAR )A 405 320 :M f0_14 sf (G)S 417 320 :M f0_12 sf -.053(RAMMARS)A 97 351 :M f2_12 sf .219 .022(An important consideration in the development of a grammatical representation)J 97 369 :M 1.851 .185(is the decidability of a number of important issues. It is known that some)J 97 387 :M .673 .067(classes of languages or grammars have most relevant issues decidable, such as)J 97 405 :M .985 .099(the nature of the language that results from language union and intersection.)J 97 423 :M 1.657 .166(Another useful attribute is the ability to construct a deterministic parser to)J 97 441 :M -.007(verify the validity of some event sequence under consideration. Turnbull showed)A 97 459 :M .93 .093(that these issues are decidable for his DRP grammars. Practical and efficient)J 97 477 :M 1.261 .126(parsers can be constructed to recognize sentences in DRP languages. In this)J 97 495 :M 2.521 .252(section, we will consider the structure of the overall module grammar )J 531 485 12 12 rC 543 497 :M psb currentpoint pse 531 485 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-BoldItalic f1 (G) -8 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 543 495 :M f2_12 sf (,)S 97 513 :M -.017(introduced in Section\3123.2.5.)A 97 543 :M .568 .057(The grammar, with all shuffle and delay productions removed and the addition)J 97 560 :M .103 .01(of an end marker on the goal production, is clearly )J 382 549 29 15 rC 411 564 :M psb currentpoint pse 382 549 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 928 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (LR) 12 292 sh 384 /Times-Roman f1 (1) 553 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1171 /Symbol f3 (\() 451 302 sh (\)) 722 302 sh end MTsave restore pse gR gS 31 31 552 730 rC 411 560 :M f2_12 sf .077 .008(. The productions are of)J 97 579 :M -.024(two forms:)A 97 609 :M (\245)S 115 609 :M .114 .011(Finite: Many of the productions in the grammar reduce to sentences that are)J 115 627 :M .532 .053(either a single terminal or a finite string of terminals. The first terminal in)J 115 645 :M -.013(each such sentence uniquely occupies this position.)A 97 675 :M (\245)S 115 675 :M .596 .06(Right Recursive: Some of the productions take the form )J 438 665 41 12 rC 479 677 :M psb currentpoint pse 438 665 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1312 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (S) -3 261 sh (AS) 773 261 sh 384 /Symbol f1 (\256) 276 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 479 675 :M f2_12 sf .677 .068(. These are)J 115 693 :M .179 .018(the only recursive productions in the grammar. Each of the symbols )J 501 683 9 12 rC 510 695 :M psb currentpoint pse 501 683 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (S) -3 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 510 693 :M f2_12 sf .086 .009( in the)J endp %%Page: 103 103 %%BeginPageSetup initializepage (nestor; page: 103 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(44)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 64 101 :M f0_13 sf -.155(3.2.5)A 109 101 :M -.011(Multi-State Representation)A 64 131 :M f2_12 sf 1.137 .114(The previous section developed the representation for a particular state )J 484 121 26 12 rC 510 133 :M psb currentpoint pse 484 121 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 832 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh (S) 531 261 sh 384 /Symbol f1 (\316) 229 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 510 131 :M f2_12 sf (.)S 64 149 :M .991 .099(We will now go on to take the grammars for each of the individual states and)J 64 167 :M .67 .067(connect them together to create a grammar )J 315 157 12 12 rC 327 169 :M psb currentpoint pse 315 157 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-BoldItalic f1 (G) -8 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 327 167 :M f2_12 sf .726 .073( for the module as it moves from)J 64 185 :M -.058(state to state.)A 64 215 :M -.014(There are a number of preliminary definitions required:)A 64 246 :M (\245)S 82 231 30 15 rC 112 246 :M psb currentpoint pse 82 231 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 960 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh (S) 674 261 sh 224 /Times-Roman f1 (0) 139 357 sh 384 /Symbol f1 (\316) 372 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 112 241 :M f2_12 sf -.026( the module\325s initial state.)A 64 277 :M (\245)S 82 264 51 13 rC 133 277 :M psb currentpoint pse 82 264 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1632 div 416 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (N) 13 261 sh (S) 752 261 sh (S) 1324 261 sh 384 /Symbol f1 (\315) 379 261 sh (\264) 1027 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 133 274 :M f2_12 sf .694 .069( the next state relation. If )J 289 261 53 20 rC 342 281 :M psb currentpoint pse 289 261 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1696 div 640 3 -1 roll exch div scale currentpoint translate 64 44 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -93 273 93 0 vb 16 th 93 273 0 273 vb 16 th 93 273 802 0 vb 16 th -93 273 895 273 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) 132 372 sh (s) 503 372 sh (N) 1324 372 sh 224 ns (i) 273 468 sh (j) 677 468 sh 384 /Times-Roman f1 (,) 368 372 sh 384 /Symbol f1 (\316) 1006 372 sh end MTsave restore pse gR gS 31 31 552 730 rC 342 274 :M f2_12 sf .66 .066( then the module can \(validly\))J 82 293 :M -.045(move from state )A 176 283 10 15 rC 186 298 :M psb currentpoint pse 176 283 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 320 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh 224 ns (i) 135 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 188 293 :M f2_12 sf -.027( to state )A 236 283 11 16 rC 247 299 :M psb currentpoint pse 236 283 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 352 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh 224 ns (j) 168 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 247 293 :M f2_12 sf (.)S 64 329 :M (\245)S 82 312 77 15 rC 159 327 :M psb currentpoint pse 82 312 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2464 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -77 194 763 0 vb 16 th 77 194 686 194 vb 16 th 77 194 2254 0 vb 16 th -77 194 2331 194 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-BoldItalic f1 (G) -8 293 sh (V) 790 293 sh (P) 1596 293 sh (A) 1994 293 sh 384 /Symbol f1 (=) 368 293 sh 384 /Times-Roman f1 (,) 1060 293 sh (,) 1445 293 sh (,) 1834 293 sh 384 /Times-Italic f1 (E) 1207 293 sh end MTsave restore pse gR gS 31 31 552 730 rC 159 323 :M f2_12 sf 2.374 .237( the grammar describing the overall module. The derived)J 82 346 :M -.03(components are defined as follows:)A 82 374 :M (\245)S 100 374 :M -.006(the non-terminal set )A 217 362 79 25 rC 217 387 :M f3_12 sf -.436( )A 296 387 :M psb currentpoint pse 217 362 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2528 div 800 3 -1 roll exch div scale currentpoint translate 64 38 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-BoldItalic f1 (V) -18 346 sh (A) 851 346 sh 384 /Symbol f1 (=) 355 346 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1182 /Symbol f3 ({) 651 359 sh (}) 1081 359 sh 384 /Symbol f1 (\310) 1322 346 sh 224 ns (\316) 1800 718 sh 384 /Times-Italic f1 (V) 2095 346 sh 224 ns (s) 2296 442 sh (s) 1696 718 sh (S) 1943 718 sh 576 /MT-Extra f1 (U) 1686 433 sh end MTsave restore pse gR gS 31 31 552 730 rC 296 374 :M f2_12 sf (,)S 82 414 :M (\245)S 100 414 :M -.043(the production set )A 204 400 220 31 rC 204 431 :M f3_12 sf -.436( )A 424 431 :M psb currentpoint pse 204 400 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 7040 div 992 3 -1 roll exch div scale currentpoint translate 64 34 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 9 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -55 164 2758 578 vb 9 th 55 164 2703 742 vb 9 th 55 164 3211 578 vb 9 th -55 164 3266 742 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-BoldItalic f1 (P) 10 414 sh (A) 847 414 sh 384 /Symbol f1 (=) 351 414 sh (\256) 1172 414 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1736 /Symbol f3 ({) 647 479 sh (}) 2085 479 sh 384 /Symbol f1 (\310) 2326 414 sh (\256) 4320 414 sh 384 1000 1924 /Symbol f3 ({) 3648 496 sh (}) 5619 496 sh 384 /Symbol f1 (\310) 5860 414 sh 224 ns (\316) 3297 799 sh (\316) 6338 786 sh 384 /Times-Italic f1 (A) 1669 414 sh (A) 3846 414 sh (A) 4817 414 sh (A) 5214 414 sh (P) 6655 414 sh 224 ns (s) 1880 510 sh (s) 4057 510 sh (s) 5028 510 sh (s) 5425 510 sh (s) 2793 799 sh (s) 3019 799 sh (N) 3450 799 sh (s) 6826 510 sh (s) 6234 786 sh (S) 6481 786 sh 160 ns (i) 4136 566 sh (i) 5107 566 sh (j) 5527 566 sh (i) 2872 855 sh (j) 3121 855 sh 160 /Times-Roman f1 (0) 1962 566 sh 224 /Times-Roman f1 (,) 2945 799 sh 576 /MT-Extra f1 (U) 2965 501 sh (U) 6224 501 sh end MTsave restore pse gR gS 31 31 552 730 rC 424 414 :M f2_12 sf (.)S 64 458 :M .334 .033(The set of terminal symbols for the global grammar is the same as that for each)J 64 476 :M 1.055 .106(of the individual state grammars. The global grammar merely takes the goal)J 64 494 :M 1.493 .149(symbols for each of the state grammars and concatenates them in a manner)J 64 512 :M 1.313 .131(consistent with the next-state relation. The entire sets of non-terminals and)J 64 530 :M 1.672 .167(productions from the individual state grammars)J f2_9 sf 0 -3 rm .3(47)A 0 3 rm f2_12 sf 1.009 .101( are included in the sets of)J 64 548 :M -.017(non-terminals and productions for the overall grammar.)A 64 578 :M .638 .064(In this way, the overall grammar )J 258 568 12 12 rC 270 580 :M psb currentpoint pse 258 568 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-BoldItalic f1 (G) -8 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 270 578 :M f2_12 sf .566 .057( generates a language whose sentences are)J 64 596 :M -.013(valid event sequences as the module moves from state to state.)A 64 626 :M .38 .038(Given the above description of modular specification, it should be apparent that)J 64 644 :M 1.404 .14(the minimum parameters for describing a module can be stated by the tuple)J -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 64 680.24 -.24 .24 207.24 680 .24 64 680 @a 64 694 :M f2_9 sf -.066(47)A f2_10 sf 0 3 rm -.055(I.e., the sets )A 0 -3 rm 133 687 12 15 rC 145 702 :M psb currentpoint pse 133 687 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (V) -16 261 sh 224 ns (s) 185 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 145 697 :M f2_10 sf -.242( and )A 168 687 12 15 rC 180 702 :M psb currentpoint pse 168 687 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (P) 6 261 sh 224 ns (s) 177 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 180 697 :M f2_10 sf -.037(, respectively.)A endp %%Page: 104 104 %%BeginPageSetup initializepage (nestor; page: 104 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 97 64 :M f1_10 sf -.018(Modular Specification)A 533 64 :M f0_12 sf -.781(43)A 97 100 :M -.03(Algorithm 3.1: Single Module Shuffle Production Set Construction)A 93 90 -1 2 95 88 1 93 88 @a -1 -2 95 90 1 2 93 88 @b 95 90 -1 2 549 88 1 95 88 @a 549 90 -1 2 551 88 1 549 88 @a -1 -2 551 90 1 2 549 88 @b -1 -2 95 103 1 2 93 90 @b -1 -2 551 103 1 2 549 90 @b 115 109 41 15 rC 156 124 :M psb currentpoint pse 115 109 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1312 div 480 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (SP) -3 276 sh 224 ns (s) 360 372 sh 384 /Symbol f1 (=) 582 276 sh (\306) 886 276 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -2 95 106 1 2 93 105 @b 95 106 -1 1 549 105 1 95 105 @a -1 -2 551 106 1 2 549 105 @b -1 -2 95 124 1 2 93 106 @b -1 -2 551 124 1 2 549 106 @b 115 151 :M f2_12 sf -.008(First add the productions within each block)A -1 -2 95 154 1 2 93 124 @b -1 -2 551 154 1 2 549 124 @b 115 155 269 20 rC 115 175 :M -.668( )A 384 175 :M psb currentpoint pse 115 155 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 8608 div 640 3 -1 roll exch div scale currentpoint translate 64 49 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") -11 431 sh (\316) 535 431 sh (\316) 2673 431 sh (*) 3223 261 sh (\316) 4268 431 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1268 /Symbol f3 (\() 6610 450 sh (\)) 6978 450 sh 384 /Symbol f1 (=) 7192 431 sh 384 /Times-Italic f1 (p) 262 431 sh (BPT) 850 431 sh (v) 1796 431 sh (x) 2115 431 sh (z) 2433 431 sh (V) 2962 431 sh (w) 3607 431 sh (y) 4012 431 sh (V) 4557 431 sh (rhs) 6120 431 sh (p) 6782 431 sh (vwxyz) 7501 431 sh 224 ns (s) 1497 527 sh (s) 3163 527 sh (s) 4758 527 sh 384 /Times-Roman f1 (,) 1616 431 sh (,) 1963 431 sh (,) 2292 431 sh (\303) 3065 324 sh (,) 3423 431 sh (,) 3861 431 sh (\303) 4660 324 sh (,) 8417 431 sh 384 /NewCenturySchlbk-Roman f1 (s.t.) 5237 431 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -2 95 175 1 2 93 154 @b -1 -2 551 175 1 2 549 154 @b 133 198 :M f0_12 sf -.278(if )A 146 176 236 38 rC 146 214 :M f3_12 sf -.436( )A 382 214 :M psb currentpoint pse 146 176 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 7552 div 1216 3 -1 roll exch div scale currentpoint translate 64 46 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -80 211 5182 348 vb 16 th 80 211 5102 559 vb 16 th 80 211 5817 348 vb 16 th -80 211 5897 559 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (w) 176 658 sh (Z) 1559 658 sh (y) 2643 658 sh (Y) 3922 658 sh (w) 5222 658 sh (y) 5627 658 sh (prereq) 6341 658 sh 224 ns (j) 1805 754 sh (s) 1958 754 sh (j) 849 1030 sh (n) 1307 1030 sh (i) 4094 754 sh (s) 4241 754 sh (i) 3195 1030 sh (m) 3650 1030 sh (s) 7363 754 sh 384 /Symbol f1 (\317) 520 658 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1664 /Symbol f3 ({) 1371 716 sh (}) 2071 716 sh 384 /Symbol f1 (\346) -15 355 sh (\350) -15 1006 sh (\347) -15 787 sh (\332) 2316 658 sh (\317) 2899 658 sh 384 1000 1578 /Symbol f3 ({) 3757 708 sh (}) 4354 708 sh 384 /Symbol f1 (\366) 4523 355 sh (\370) 4523 1006 sh (\367) 4523 787 sh (\331) 4783 658 sh (\317) 6008 658 sh 224 ns (\316) 935 1030 sh 224 1000 1227 /Symbol f3 ([) 1061 1045 sh (]) 1434 1045 sh 224 /Symbol f1 (\316) 3275 1030 sh 224 1000 1227 /Symbol f3 ([) 3401 1045 sh (]) 3828 1045 sh 224 /Times-Roman f1 (,) 1884 754 sh (,) 1235 1030 sh (,) 4167 754 sh (,) 3575 1030 sh 384 ns (,) 5476 658 sh 224 /Times-Roman f1 (1) 1132 1030 sh (1) 3472 1030 sh 576 /MT-Extra f1 (U) 968 745 sh (U) 3354 745 sh end MTsave restore pse gR gS 31 31 552 730 rC 382 198 :M f0_12 sf -.222( then)A 414 198 :M f2_12 sf ( )S 417 187 115 16 rC 532 203 :M psb currentpoint pse 417 187 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3680 div 512 3 -1 roll exch div scale currentpoint translate 64 43 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (SP) -3 309 sh (SP) 897 309 sh (wy) 1986 309 sh (yw) 2987 309 sh 224 ns (s) 360 405 sh (s) 1260 405 sh 384 /Symbol f1 (=) 582 309 sh (\310) 1455 309 sh (\256) 2497 309 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1286 /Symbol f3 ({) 1810 331 sh (}) 3405 331 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -2 95 214 1 2 93 175 @b -1 -2 551 214 1 2 549 175 @b 115 241 :M f2_12 sf -.007(Now add the inter-block shuffle productions)A -1 -2 95 244 1 2 93 214 @b -1 -2 551 244 1 2 549 214 @b 115 245 341 37 rC 115 282 :M -.668( )A 456 282 :M psb currentpoint pse 115 245 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 10912 div 1184 3 -1 roll exch div scale currentpoint translate 64 63 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") -11 431 sh (\316) 627 431 sh (-) 1562 431 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) 899 454 sh (]) 1989 454 sh 384 /Symbol f1 (\316) 2624 431 sh (+) 3396 431 sh (\316) 5359 431 sh (\316) 7899 431 sh (*) 8449 261 sh (\316) 9403 431 sh 384 1000 1369 /Symbol f3 (\() 1801 959 sh (\)) 2275 959 sh 384 /Symbol f1 (=) 2489 931 sh (\331) 3426 931 sh 384 1000 1369 /Symbol f3 (\() 4193 959 sh (\)) 4703 959 sh 384 /Symbol f1 (=) 4917 931 sh (\331) 5880 931 sh 384 1000 1369 /Symbol f3 (\() 6680 959 sh (\)) 7154 959 sh 384 /Symbol f1 (=) 7368 931 sh (\331) 8369 931 sh 384 1000 1369 /Symbol f3 (\() 9169 959 sh (\)) 9679 959 sh 384 /Symbol f1 (=) 9893 931 sh 384 /Times-Italic f1 (k) 262 431 sh (b) 1288 431 sh (k) 2223 431 sh (k) 3033 431 sh (b) 3944 431 sh (p) 4486 431 sh (p) 4944 431 sh (BPT) 5674 431 sh (u) 6613 431 sh (w) 6935 431 sh (x) 7341 431 sh (z) 7659 431 sh (V) 8188 431 sh (v) 8829 431 sh (y) 9147 431 sh (V) 9692 431 sh (lhs) 1354 931 sh (p) 1973 931 sh (T) 2795 931 sh (lhs) 3746 931 sh (p) 4365 931 sh (T) 5223 931 sh (rhs) 6190 931 sh (p) 6852 931 sh (uvw) 7670 931 sh (rhs) 8679 931 sh (p) 9341 931 sh (xyz) 10222 931 sh 224 ns (s) 6321 527 sh (s) 8389 527 sh (s) 9893 527 sh (k) 2974 1028 sh (s) 3224 1028 sh (k) 5402 1028 sh (s) 5678 1028 sh 224 /Times-Roman f1 (1) 412 527 sh (2) 2391 527 sh (1) 3183 527 sh (1) 4650 527 sh (2) 5126 527 sh (1) 2137 1027 sh (2) 4547 1027 sh (1) 7016 1027 sh (2) 9523 1027 sh 384 ns (1) 1000 431 sh (1) 1821 431 sh (1) 3656 431 sh 160 ns (1) 3056 1084 sh (2) 5497 1084 sh 384 /Times-Roman f1 (,) 1156 431 sh (,) 2088 431 sh ([) 2896 431 sh (,) 3812 431 sh (],) 4142 431 sh (,) 4775 431 sh (,) 6440 431 sh (,) 6799 431 sh (,) 7189 431 sh (,) 7518 431 sh (\303) 8291 324 sh (,) 8649 431 sh (,) 8996 431 sh (\303) 9795 324 sh (,) 10712 931 sh 224 ns (,) 3150 1028 sh (,) 5604 1028 sh 384 /NewCenturySchlbk-Roman f1 (s.t.) 365 931 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -2 95 282 1 2 93 244 @b -1 -2 551 282 1 2 549 244 @b 133 305 :M f0_12 sf -.163(if)A f2_12 sf ( )S 145 283 147 38 rC 145 321 :M f3_12 sf -.436( )A 292 321 :M psb currentpoint pse 145 283 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4704 div 1216 3 -1 roll exch div scale currentpoint translate 64 46 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (v) 172 658 sh (Z) 1468 658 sh (y) 2552 658 sh (Y) 3831 658 sh 224 ns (j) 1714 754 sh (s) 1867 754 sh (j) 758 1030 sh (n) 1216 1030 sh (i) 4003 754 sh (s) 4150 754 sh (i) 3104 1030 sh (m) 3559 1030 sh 384 /Symbol f1 (\317) 429 658 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1664 /Symbol f3 ({) 1280 716 sh (}) 1980 716 sh 384 /Symbol f1 (\346) -15 355 sh (\350) -15 1006 sh (\347) -15 787 sh (\332) 2225 658 sh (\317) 2808 658 sh 384 1000 1578 /Symbol f3 ({) 3666 708 sh (}) 4263 708 sh 384 /Symbol f1 (\366) 4432 355 sh (\370) 4432 1006 sh (\367) 4432 787 sh 224 ns (\316) 844 1030 sh 224 1000 1227 /Symbol f3 ([) 970 1045 sh (]) 1343 1045 sh 224 /Symbol f1 (\316) 3184 1030 sh 224 1000 1227 /Symbol f3 ([) 3310 1045 sh (]) 3737 1045 sh 224 /Times-Roman f1 (,) 1793 754 sh (,) 1144 1030 sh (,) 4076 754 sh (,) 3484 1030 sh 224 /Times-Roman f1 (1) 1041 1030 sh (1) 3381 1030 sh 576 /MT-Extra f1 (U) 877 745 sh (U) 3263 745 sh end MTsave restore pse gR gS 31 31 552 730 rC 292 305 :M f0_12 sf -.222( then)A 324 305 :M f2_12 sf ( )S 327 294 109 16 rC 436 310 :M psb currentpoint pse 327 294 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3488 div 512 3 -1 roll exch div scale currentpoint translate 64 43 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (SP) -3 309 sh (SP) 897 309 sh (vy) 1982 309 sh (yv) 2897 309 sh 224 ns (s) 360 405 sh (s) 1260 405 sh 384 /Symbol f1 (=) 582 309 sh (\310) 1455 309 sh (\256) 2407 309 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1286 /Symbol f3 ({) 1810 331 sh (}) 3228 331 sh end MTsave restore pse gR gS 31 31 552 730 rC 93 323 -1 2 95 321 1 93 321 @a -1 -2 95 323 1 2 93 321 @b 95 323 -1 2 549 321 1 95 321 @a 549 323 -1 2 551 321 1 549 321 @a -1 -2 551 323 1 2 549 321 @b -1 -2 95 321 1 2 93 282 @b -1 -2 551 321 1 2 549 282 @b 97 348 :M f2_12 sf 3.336 .334(The set of shuffle productions )J 292 338 17 15 rC 309 353 :M psb currentpoint pse 292 338 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (SP) -3 261 sh 224 ns (s) 360 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 309 348 :M f2_12 sf 3.531 .353( is based upon the set of transaction)J 97 366 :M 1.223 .122(productions )J 168 356 27 15 rC 195 371 :M psb currentpoint pse 168 356 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 864 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPT) 10 261 sh 224 ns (s) 657 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 195 366 :M f2_12 sf 1.693 .169( and the prerequisite relation )J 376 356 39 15 rC 415 371 :M psb currentpoint pse 376 356 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1248 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (prereq) 28 261 sh 224 ns (s) 1050 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 415 366 :M f2_12 sf 1.985 .198(. We must be careful)J 97 386 :M 1.3 .13(when defining the set of shuffle productions. The percolation of events must)J 97 404 :M .527 .053(occur in a single direction, so that circular derivation paths are not created. In)J 97 422 :M 1.338 .134(addition, the grammar that results must be unambiguous, so that each valid)J 97 440 :M .387 .039(sentence in the language has only a single derivation. Such constraints become)J 97 458 :M 2.024 .202(important if one wishes to construct a parser that will recognize sentences)J 97 476 :M -.019(generated by the module grammar.)A 97 506 :M .897 .09(The combined effect of the delay and shuffle productions is that output events)J 97 524 :M .569 .057(can jump over both input events and output events, and input events can jump)J 97 542 :M 1.274 .127(over other input events. Input events can jump over output events, but only)J 97 560 :M -.002(when there is no possibility of violating temporal restrictions.)A 97 590 :M .81 .081(We can consider the basic grammars to be a normal form, with the addition of)J 97 608 :M 1.284 .128(delay and shuffle productions being used to create variations on these forms.)J 97 626 :M .562 .056(When we consider composition of grammars, we will create a composite normal)J 97 644 :M .136 .014(form grammar from the elements of the composition, then add appropriate delay)J 97 662 :M -.027(and shuffle production rules.)A endp %%Page: 105 105 %%BeginPageSetup initializepage (nestor; page: 105 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(42)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 64 100 :M f2_12 sf .533 .053(various modules, delay productions are used to allow for situations in which an)J 64 118 :M 2.507 .251(output event may be delayed until after several \(later\) input events have)J 64 136 :M .515 .052(occurred. Such a delay might represent the propagation delay within a module)J 64 154 :M -.007(or the amount of processing time required for a particular type of input event.)A 64 184 :M -.006(The set of delay productions is given by)A 217 200 140 35 rC 217 235 :M f3_12 sf -.436( )A 357 235 :M psb currentpoint pse 217 200 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4480 div 1120 3 -1 roll exch div scale currentpoint translate 64 45 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (DP) 10 371 sh (Z) 1758 371 sh (Y) 2255 371 sh (Y) 3246 371 sh (Z) 3686 371 sh 224 ns (s) 458 467 sh (j) 2004 467 sh (s) 2157 467 sh (i) 2427 467 sh (s) 2574 467 sh (i) 3418 467 sh (s) 3565 467 sh (j) 3932 467 sh (s) 4085 467 sh (i) 1028 743 sh (m) 1483 743 sh (j) 1022 967 sh (n) 1480 967 sh 384 /Symbol f1 (=) 680 371 sh (\256) 2782 371 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1664 /Symbol f3 ({) 1570 429 sh (}) 4198 429 sh 224 /Symbol f1 (\316) 1108 743 sh (\316) 1108 967 sh 224 /Times-Roman f1 (,) 2083 467 sh (,) 2500 467 sh (,) 3491 467 sh (,) 4011 467 sh ([) 1234 743 sh (,) 1408 743 sh (]) 1661 743 sh ([) 1234 967 sh (,) 1408 967 sh (]) 1607 967 sh 224 /Times-Roman f1 (1) 1305 743 sh (1) 1305 967 sh 576 /MT-Extra f1 (U) 1167 458 sh end MTsave restore pse gR gS 31 31 552 730 rC 357 217 :M f2_12 sf (.)S 64 262 :M -.01(An output may always be delayed past a later input while in a particular state.)A 64 290 :M f0_13 sf -.155(3.2.4)A 109 290 :M -.016(Shuffle Production Set)A 64 318 :M f2_12 sf 1.486 .149(Finally, there are the )J 196 318 :M f1_12 sf 1.605 .16(shuffle productions )J f2_12 sf .944 .094(\(the set )J 360 308 17 15 rC 377 323 :M psb currentpoint pse 360 308 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (SP) -3 261 sh 224 ns (s) 360 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 377 318 :M f2_12 sf 1.47 .147(\). In more complicated)J 64 338 :M 2.256 .226(modules and compositions, we may have multiple independent)J f2_9 sf 0 -3 rm .417(46)A 0 3 rm f2_12 sf 1.652 .165( input and)J 64 356 :M 1.073 .107(output event sequences. Because the sequences are independent, the relative)J 64 374 :M .357 .036(ordering of events from each sequence is not important. The shuffle rules allow)J 64 392 :M 2.014 .201(these independent sequences to be freely intermixed. In effect, the shuffle)J 64 410 :M .426 .043(productions are used to override artifacts of the particular ordering specified by)J 64 428 :M .456 .046(the basic productions. Independent events must be ordered in a particular way)J 64 446 :M .872 .087(in the transaction productions. The shuffle rules eliminate this original, fixed)J 64 464 :M -.002(order where no ordering need be enforced.)A 64 492 :M .211 .021(The set of shuffle productions )J 233 482 17 15 rC 250 497 :M psb currentpoint pse 233 482 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (SP) -3 261 sh 224 ns (s) 360 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 250 492 :M f2_12 sf .163 .016(, is constructed through a two-stage process, as)J 64 512 :M .243 .024(described in Algorithm\3123.1. First shuffling within blocks is handled, followed by)J 64 530 :M -.042(shuffling between blocks.)A -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 64 659.24 -.24 .24 207.24 659 .24 64 659 @a 64 672 :M f2_9 sf .376(46)A f2_10 sf 0 3 rm 1.36 .136(By independent, we mean that there is no causal relationship between events in the two)J 0 -3 rm 64 687 :M .384 .038(sequences )J f1_10 sf .362 .036(within the module)J 200 687 :M f2_10 sf .704 .07(. For example, events representing the appearance of each of the)J 64 699 :M -.009(operands to an adder circuit are independent in the sense understood here.)A endp %%Page: 106 106 %%BeginPageSetup initializepage (nestor; page: 106 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 97 64 :M f1_10 sf -.018(Modular Specification)A 535 64 :M f0_12 sf -1.781(41)A 97 100 :M -.06(Requirement 3.5:)A 99 116 446 42 rC 99 158 :M f2_12 sf -.668( )A 545 158 :M psb currentpoint pse 99 116 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 14272 div 1344 3 -1 roll exch div scale currentpoint translate 64 35 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -80 211 464 638 vb 16 th 80 211 384 849 vb 16 th 80 211 1099 638 vb 16 th -80 211 1179 849 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") -11 270 sh (\316) 497 270 sh (\316) 1834 270 sh (\316) 1290 948 sh (\336) 2854 948 sh ($) 3504 948 sh (\316) 3987 948 sh (\316) 6125 948 sh (*) 6675 778 sh (\316) 7518 948 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1268 /Symbol f3 (\() 9860 967 sh (\)) 10228 967 sh 384 /Symbol f1 (=) 10442 948 sh (\331) 11622 948 sh (\336) 12084 948 sh (\331) 12846 948 sh (\336) 13377 948 sh (\346) 3317 784 sh (\350) 3317 1157 sh (\366) 13987 784 sh (\370) 13987 1157 sh 384 /Times-Italic f1 (s) 262 270 sh (S) 799 270 sh (w) 1173 270 sh (y) 1578 270 sh (E) 2145 270 sh (w) 504 948 sh (y) 909 948 sh (prereq) 1623 948 sh (p) 3714 948 sh (BPT) 4302 948 sh (v) 5248 948 sh (x) 5567 948 sh (z) 5885 948 sh (V) 6414 948 sh (t) 7002 948 sh (u) 7242 948 sh (V) 7807 948 sh (rhs) 9370 948 sh (p) 10032 948 sh (vtxuz) 10751 948 sh (t) 11927 948 sh (w) 12509 948 sh (u) 13149 948 sh (y) 13817 948 sh 224 ns (s) 2645 1044 sh (s) 4949 1044 sh (s) 6615 1044 sh (s) 8008 1044 sh (G) 12159 1179 sh (G) 13452 1179 sh 160 ns (s) 12311 1235 sh (s) 13604 1235 sh 384 /Times-Roman f1 (,) 989 270 sh (,) 1427 270 sh (,) 2383 270 sh (,) 758 948 sh (,) 5068 948 sh (,) 5415 948 sh (,) 5744 948 sh (\303) 6517 841 sh (,) 6875 948 sh (,) 7117 948 sh (\303) 7910 841 sh 384 /NewCenturySchlbk-Roman f1 (s.t.) 8487 948 sh end MTsave restore pse gR gS 31 31 552 730 rC 97 185 :M f2_12 sf 2.593 .259(If two events are temporally related, then there must exist a transaction)J 97 203 :M .988 .099(production that enforces this relation. Events from different blocks cannot be)J 97 221 :M -.013(temporally related.)A 97 251 :M -.009(We will now formalize a notion relating to the block structure. If we consider the)A 97 269 :M 3.068 .307(graphical representation \(mentioned at the beginning of Section\3123.2.2\) of)J 97 285 :M 1.43 .143(temporal event ordering as defined by the )J 348 275 39 15 rC 387 290 :M psb currentpoint pse 348 275 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1248 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (prereq) 28 261 sh 224 ns (s) 1050 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 387 285 :M f2_12 sf 1.445 .145( relation, we can break the)J 97 305 :M 4.409 .441(graph into weakly connected components. Each of these components)J 97 323 :M .95 .095(corresponds to a block. In the specification of a modular grammar, blocks are)J 97 341 :M .464 .046(defined by transaction productions that share common non-terminal symbols in)J 97 359 :M -.03(their right-hand sides.)A 97 389 :M 9.046 .905(For example, a module with )J 325 379 28 12 rC 353 391 :M psb currentpoint pse 325 379 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (b) -9 261 sh 384 /Symbol f1 (=) 281 261 sh 384 /Times-Roman f1 (2) 588 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 353 389 :M f2_12 sf 7.116 .712(, transaction production set)J 97 393 117 32 rC 214 425 :M psb currentpoint pse 97 393 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3744 div 1024 3 -1 roll exch div scale currentpoint translate 64 50 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPT) 10 558 sh (T) 1413 293 sh (Y) 2420 293 sh (Z) 2875 293 sh (T) 1377 758 sh (Y) 2420 758 sh (Z) 2911 758 sh 224 ns (s) 657 654 sh (s) 1748 389 sh (s) 2754 389 sh (s) 3250 389 sh (s) 1748 854 sh (s) 2790 854 sh (s) 3322 854 sh 384 /Symbol f1 (=) 879 558 sh (\256) 1956 293 sh (\256) 1956 758 sh (\354) 1192 355 sh (\355) 1192 623 sh (\356) 1192 892 sh (\374) 3459 355 sh (\375) 3459 623 sh (\376) 3459 892 sh 224 /Times-Roman f1 (1) 1571 389 sh (1) 2577 389 sh (1) 3073 389 sh (2) 1553 854 sh (2) 2595 854 sh (2) 3127 854 sh 224 /Times-Roman f1 (,) 1674 389 sh (,) 2680 389 sh (,) 3176 389 sh (,) 1674 854 sh (,) 2716 854 sh (,) 3248 854 sh end MTsave restore pse gR gS 31 31 552 730 rC 214 412 :M f2_12 sf 4.992 .499( and prerequisite relation with )J 429 400 85 17 rC 514 417 :M psb currentpoint pse 429 400 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2720 div 544 3 -1 roll exch div scale currentpoint translate 64 58 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -83 227 83 0 vb 16 th 83 227 0 227 vb 16 th 83 227 964 0 vb 16 th -83 227 1047 227 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 98 326 sh (b) 611 326 sh 224 /Times-Roman f1 (1) 350 422 sh (1) 815 422 sh 384 /Times-Roman f1 (,) 475 326 sh 384 /Symbol f1 (\316) 1158 326 sh 384 /Times-Italic f1 (prereq) 1491 326 sh 224 ns (s) 2513 422 sh end MTsave restore pse gR gS 31 31 552 730 rC 514 412 :M f2_12 sf 5.978 .598( and)J 97 426 87 17 rC 184 443 :M psb currentpoint pse 97 426 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2784 div 544 3 -1 roll exch div scale currentpoint translate 64 58 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -83 227 83 0 vb 16 th 83 227 0 227 vb 16 th 83 227 1036 0 vb 16 th -83 227 1119 227 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 98 326 sh (b) 647 326 sh 224 /Times-Roman f1 (2) 368 422 sh (2) 869 422 sh 384 /Times-Roman f1 (,) 511 326 sh 384 /Symbol f1 (\316) 1230 326 sh 384 /Times-Italic f1 (prereq) 1563 326 sh 224 ns (s) 2585 422 sh end MTsave restore pse gR gS 31 31 552 730 rC 184 470 :M f2_12 sf 1.666 .167( )J 190 438 :M 1.456 .146(has two separate blocks. This leads to the following general)J 97 458 :M -.04(requirement:)A 97 488 :M f0_12 sf -.06(Requirement 3.6:)A 147 504 350 40 rC 497 544 :M psb currentpoint pse 147 504 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 11200 div 1280 3 -1 roll exch div scale currentpoint translate 64 51 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") 1338 431 sh (\316) 1846 431 sh (\316) 2793 431 sh (\316) 4334 431 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) 4606 454 sh (]) 5194 454 sh 384 /Symbol f1 (\316) 6383 431 sh (\316) 8911 431 sh (*) 9461 261 sh 384 1000 1369 /Symbol f3 (\() 556 1016 sh (\)) 1030 1016 sh 384 /Symbol f1 (=) 1244 988 sh (\331) 2181 988 sh 384 1000 1369 /Symbol f3 (\() 2932 1016 sh (\)) 3442 1016 sh 384 /Symbol f1 (=) 3656 988 sh (\331) 4619 988 sh 384 1000 1369 /Symbol f3 (\() 5419 1016 sh (\)) 5893 1016 sh 384 /Symbol f1 (=) 6107 988 sh (\331) 7093 988 sh 384 1000 1369 /Symbol f3 (\() 7893 1016 sh (\)) 8403 1016 sh 384 /Symbol f1 (=) 8617 988 sh 384 1000 1713 /Symbol f3 (\() -20 1048 sh (\)) 9449 1048 sh 384 /Symbol f1 (\336) 9650 988 sh (=) 10500 988 sh 384 /Times-Italic f1 (s) 1611 431 sh (S) 2148 431 sh (y) 2537 431 sh (V) 3082 431 sh (k) 3523 431 sh (k) 3933 431 sh (b) 4995 431 sh (p) 5510 431 sh (p) 5968 431 sh (BPT) 6698 431 sh (v) 7644 431 sh (w) 7947 431 sh (x) 8353 431 sh (z) 8671 431 sh (V) 9200 431 sh (lhs) 109 988 sh (p) 728 988 sh (T) 1550 988 sh (lhs) 2485 988 sh (p) 3104 988 sh (T) 3962 988 sh (rhs) 4929 988 sh (p) 5591 988 sh (vyw) 6416 988 sh (rhs) 7403 988 sh (p) 8065 988 sh (xyz) 8946 988 sh (k) 10122 988 sh (k) 10812 988 sh 224 ns (s) 7345 527 sh (s) 9401 527 sh (k) 1729 1085 sh (s) 1979 1085 sh (k) 4141 1085 sh (s) 4417 1085 sh 384 /Times-Roman f1 (,) 2338 431 sh (\303) 3185 324 sh (,) 3340 431 sh (,) 3798 431 sh (,) 4863 431 sh (,) 5293 431 sh (,) 5799 431 sh (,) 7464 431 sh (,) 7811 431 sh (,) 8201 431 sh (,) 8530 431 sh (\303) 9303 324 sh (,) 9661 431 sh 224 ns (,) 1905 1085 sh (,) 4343 1085 sh 224 /Times-Roman f1 (1) 3673 527 sh (2) 4101 527 sh (1) 5674 527 sh (2) 6150 527 sh (1) 892 1084 sh (2) 3286 1084 sh (1) 5755 1084 sh (2) 8247 1084 sh (1) 10272 1084 sh (2) 10980 1084 sh 384 ns (1) 4707 431 sh 160 ns (1) 1811 1141 sh (2) 4236 1141 sh end MTsave restore pse gR gS 31 31 552 730 rC 97 571 :M f2_12 sf .555 .056(If two transaction productions have an input or an output non-terminal symbol)J 97 589 :M .741 .074(in common in their right hand sides, then they must be part of the same block)J 97 607 :M -.011(\(i.e., have the same assigned block numbers\).)A 97 635 :M f0_13 sf -.155(3.2.3)A 142 635 :M -.023(Delay Production Set)A 97 665 :M f2_12 sf 1.906 .191(To account for the queueing of input events, the basic productions must be)J 97 681 :M -.017(augmented with one or more )A 260 681 :M f1_12 sf -.017(delay productions )A 362 681 :M f2_12 sf .055 .005(\(contained in the set )J 479 671 20 15 rC 499 686 :M psb currentpoint pse 479 671 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 640 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (DP) 10 261 sh 224 ns (s) 458 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 499 681 :M f2_12 sf -.061(\). In the)A endp %%Page: 107 107 %%BeginPageSetup initializepage (nestor; page: 107 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(40)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 64 100 :M f2_12 sf 1.055 .105(The following requirements restrict the type of prerequisite relations that are)J 64 118 :M -.008(valid under our specification technique.)A 64 148 :M f0_12 sf -.06(Requirement 3.3:)A 211 165 155 16 rC 366 181 :M psb currentpoint pse 211 165 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4960 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -77 194 2546 0 vb 16 th 77 194 2469 194 vb 16 th 77 194 3234 0 vb 16 th -77 194 3311 194 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") -11 293 sh (\316) 497 293 sh (\316) 1459 293 sh (\317) 3422 293 sh 384 /Times-Italic f1 (s) 262 293 sh (S) 799 293 sh (E) 1770 293 sh (prereq) 3755 293 sh 224 ns (s) 4777 389 sh 384 /Times-Roman f1 (,) 989 293 sh (,) 2008 293 sh (,) 2830 293 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 1100 293 sh (a) 2561 293 sh (a) 2941 293 sh end MTsave restore pse gR gS 31 31 552 730 rC 64 208 :M f2_12 sf -.015(No \(externally visible\) event is ever a prerequisite of itself.)A 389 205 :M f2_9 sf (44)S 64 238 :M f2_12 sf 2.556 .256(For convenience, we will sometimes use input or output non-terminals as)J 64 256 :M 2.492 .249(arguments to the prerequisite relation. In this case, we define the value)J 64 274 :M .196 .02(returned to be identical to the value that would be returned if the corresponding)J 64 292 :M -.016(terminal symbols were used as arguments. In other words,)A 131 308 312 92 rC 443 400 :M psb currentpoint pse 131 308 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 9984 div 2944 3 -1 roll exch div scale currentpoint translate 64 56 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -95 283 3829 429 vb 16 th 95 283 3734 712 vb 16 th 95 283 4847 429 vb 16 th -95 283 4942 712 vb 16 th -95 283 7223 429 vb 16 th 95 283 7128 712 vb 16 th 95 283 8079 429 vb 16 th -95 283 8174 712 vb 16 th -93 273 3916 1053 vb 16 th 93 273 3823 1326 vb 16 th 93 273 4806 1053 vb 16 th -93 273 4899 1326 vb 16 th -93 273 7178 1053 vb 16 th 93 273 7085 1326 vb 16 th 93 273 7993 1053 vb 16 th -93 273 8086 1326 vb 16 th -93 273 3916 1657 vb 16 th 93 273 3823 1930 vb 16 th 93 273 4806 1657 vb 16 th -93 273 4899 1930 vb 16 th -93 273 7178 1657 vb 16 th 93 273 7085 1930 vb 16 th 93 273 7993 1657 vb 16 th -93 273 8086 1930 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") -11 270 sh (\316) 497 270 sh (") 817 811 sh (\316) 1741 811 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) 2013 834 sh (]) 2692 834 sh 384 /Symbol f1 (\316) 5053 811 sh (\333) 6624 811 sh (\316) 8285 811 sh (") 373 1425 sh (\316) 841 1425 sh 384 1000 1223 /Symbol f3 ([) 1113 1448 sh (]) 1792 1448 sh 384 /Symbol f1 (\316) 2278 1425 sh 384 1000 1223 /Symbol f3 ([) 2550 1448 sh (]) 3137 1448 sh 384 /Symbol f1 (\316) 5010 1425 sh (\333) 6581 1425 sh (\316) 8197 1425 sh (") 373 2029 sh (\316) 841 2029 sh 384 1000 1223 /Symbol f3 ([) 1113 2052 sh (]) 1792 2052 sh 384 /Symbol f1 (\316) 2278 2029 sh 384 1000 1223 /Symbol f3 ([) 2550 2052 sh (]) 3137 2052 sh 384 /Symbol f1 (\316) 5010 2029 sh (\333) 6581 2029 sh (\316) 8197 2029 sh (") 825 2643 sh (\316) 1826 2643 sh 384 1000 1223 /Symbol f3 ([) 2098 2666 sh 384 /Times-Italic f1 (s) 262 270 sh (S) 799 270 sh (i) 1090 811 sh (i) 1415 811 sh (m) 2407 811 sh (prereq) 5386 811 sh (Y) 7252 811 sh (Y) 7703 811 sh (prereq) 8618 811 sh (i) 646 1425 sh (m) 1507 1425 sh (j) 2073 1425 sh (n) 2940 1425 sh (prereq) 5343 1425 sh (Y) 7207 1425 sh (Z) 7622 1425 sh (prereq) 8530 1425 sh (i) 646 2029 sh (m) 1507 2029 sh (j) 2073 2029 sh (n) 2940 2029 sh (prereq) 5343 2029 sh (Z) 7230 2029 sh (Y) 7702 2029 sh (prereq) 8530 2029 sh (j) 1098 2643 sh (j) 1490 2643 sh (n) 2488 2643 sh 224 ns (i) 4111 907 sh (i) 4643 907 sh (s) 6408 907 sh (i) 7424 907 sh (i) 7875 907 sh (s) 9640 907 sh (i) 4198 1521 sh (j) 4681 1521 sh (s) 6365 1521 sh (i) 7379 1521 sh (j) 7868 1521 sh (s) 9552 1521 sh (j) 4208 2125 sh (i) 4687 2125 sh (s) 6365 2125 sh (j) 7476 2125 sh (i) 7874 2125 sh (s) 9552 2125 sh 384 /Times-Roman f1 (,) 989 270 sh (,) 1290 811 sh (,) 2270 811 sh (,) 4265 811 sh (,) 7578 811 sh (,) 1370 1425 sh (,) 1891 1425 sh (,) 2807 1425 sh (,) 4293 1425 sh (,) 7474 1425 sh (,) 1370 2029 sh (,) 1891 2029 sh (,) 2807 2029 sh (,) 4309 2029 sh (,) 7577 2029 sh (,) 1308 2643 sh (,) 2355 2643 sh 224 /Times-Roman f1 (1) 1165 907 sh (2) 1508 907 sh (1) 1183 2739 sh (2) 1593 2739 sh 384 ns (1) 2114 811 sh (1) 1214 1425 sh (1) 2651 1425 sh (1) 1214 2029 sh (1) 2651 2029 sh (1) 2199 2643 sh 160 ns (1) 4149 963 sh (2) 4694 963 sh (1) 7462 963 sh (2) 7926 963 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 3844 811 sh (a) 4376 811 sh (a) 3931 1425 sh (b) 4429 1425 sh (b) 3956 2029 sh (a) 4420 2029 sh 16 th -95 283 3710 2261 vb 16 th 95 283 3615 2544 vb 16 th 95 283 4760 2261 vb 16 th -95 283 4855 2544 vb 16 th -95 283 7136 2261 vb 16 th 95 283 7041 2544 vb 16 th 95 283 8198 2261 vb 16 th -95 283 8293 2544 vb 384 1000 1223 /Symbol f3 (]) 2685 2666 sh (]) 2685 2666 sh 384 /Symbol f1 (\316) 4966 2643 sh (\333) 6537 2643 sh (\316) 8404 2643 sh 384 /Symbol f2 (b) 3750 2643 sh (b) 4298 2643 sh 224 /Times-Italic f1 (j) 4002 2739 sh (j) 4550 2739 sh (s) 6321 2739 sh (j) 7434 2739 sh (j) 7988 2739 sh (s) 9759 2739 sh 384 ns (prereq) 5299 2643 sh (Z) 7188 2643 sh (Z) 7742 2643 sh (prereq) 8737 2643 sh 160 /Times-Roman f1 (1) 4046 2795 sh (2) 4607 2795 sh (1) 7478 2795 sh (2) 8045 2795 sh 384 /Times-Roman f1 (,) 4162 2643 sh (,) 7594 2643 sh end MTsave restore pse gR gS 31 31 552 730 rC 443 361 :M f2_12 sf (.)S 64 427 :M f0_12 sf -.06(Requirement 3.4:)A 197 443 184 32 rC 381 475 :M psb currentpoint pse 197 443 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 5888 div 1024 3 -1 roll exch div scale currentpoint translate 64 40 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -81 217 3472 466 vb 16 th 81 217 3391 683 vb 16 th 81 217 4147 466 vb 16 th -81 217 4228 683 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") -11 270 sh (\316) 497 270 sh (\316) 741 782 sh (\331) 1508 782 sh (\316) 2073 782 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1539 /Symbol f3 (\() 364 826 sh (\)) 2712 826 sh 384 /Symbol f1 (\336) 2913 782 sh (\317) 4339 782 sh 384 /Times-Italic f1 (s) 262 270 sh (S) 799 270 sh (E) 1187 782 sh (E) 2461 782 sh (prereq) 4672 782 sh 224 ns (O) 1053 612 sh (I) 2399 612 sh (s) 5694 878 sh 384 /Times-Roman f1 (,) 989 270 sh (,) 3743 782 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) 503 782 sh (a) 1797 782 sh (b) 3512 782 sh (a) 3854 782 sh end MTsave restore pse gR gS 31 31 552 730 rC 64 502 :M f2_12 sf .292 .029(No \(externally visible\) output event can ever be a prerequisite for an \(externally)J 64 520 :M -.02(visible\) input event.)A f2_9 sf 0 -3 rm (45)S 0 3 rm 64 550 :M f2_12 sf .142 .014(The transaction productions must be consistent with the prerequisite relation as)J 64 568 :M .083 .008(defined above. If an input event non-terminal and an output event non-terminal)J 64 586 :M 2.341 .234(are temporally related and appear in the right hand side of a transaction)J 64 602 :M -.055(production, then )A 159 592 39 15 rC 198 607 :M psb currentpoint pse 159 592 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1248 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (prereq) 28 261 sh 224 ns (s) 1050 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 198 602 :M f2_12 sf -.027( must be defined appropriately.)A -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 64 633.24 -.24 .24 207.24 633 .24 64 633 @a 64 646 :M f2_9 sf .191(44)A f2_10 sf 0 3 rm .607 .061(This is the case for all externally visible input and output events \(i.e. all elements of the set)J 0 -3 rm 64 653 11 10 rC 75 663 :M psb currentpoint pse 64 653 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 352 div 320 3 -1 roll exch div scale currentpoint translate 64 27 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (E) 6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 75 662 :M f2_10 sf .671 .067(\). When we consider feedback composition in Chapter\3124, it will become possible for internal)J 64 674 :M -.016(events to cause themselves.)A 64 684 :M f2_9 sf .051(45)A f2_10 sf 0 3 rm .2 .02(Once again, this requirement will not apply to internal events when composition is considered)J 0 -3 rm 64 699 :M -.018(in Chapter\3124.)A endp %%Page: 108 108 %%BeginPageSetup initializepage (nestor; page: 108 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 97 64 :M f1_10 sf -.018(Modular Specification)A 533 64 :M f0_12 sf -.781(39)A 97 100 :M f2_12 sf .46 .046(The symbols forming the right-hand side of any transaction production must be)J 97 118 :M 1.357 .136(ordered so that all input non-terminal symbols appear before all output non)J 543 118 :M (-)S 97 136 :M -.036(terminal symbols.)A 97 166 :M f0_12 sf -.06(Requirement 3.2:)A 229 182 186 37 rC 415 219 :M psb currentpoint pse 229 182 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 5952 div 1184 3 -1 roll exch div scale currentpoint translate 64 61 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") -11 431 sh (\316) 497 431 sh (\316) 1479 431 sh (\316) 3617 431 sh (*) 4167 261 sh (\316) 5164 431 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1268 /Symbol f3 (\() 1558 965 sh (\)) 1926 965 sh 384 /Symbol f1 (=) 2140 946 sh 384 1000 1460 /Symbol f3 (\() 933 982 sh (\)) 3378 982 sh 384 /Symbol f1 (\336) 3579 946 sh (\271) 4408 946 sh 384 /Times-Italic f1 (s) 262 431 sh (S) 799 431 sh (p) 1206 431 sh (BPT) 1794 431 sh (v) 2740 431 sh (x) 3059 431 sh (z) 3377 431 sh (V) 3906 431 sh (w) 4503 431 sh (y) 4908 431 sh (V) 5453 431 sh (rhs) 1068 946 sh (p) 1730 946 sh (vwxyz) 2449 946 sh (w) 4052 946 sh (y) 4737 946 sh 224 ns (s) 2441 527 sh (s) 4107 527 sh (s) 5654 527 sh 384 /Times-Roman f1 (,) 989 431 sh (,) 2560 431 sh (,) 2907 431 sh (,) 3236 431 sh (\303) 4009 324 sh (,) 4367 431 sh (,) 4757 431 sh (\303) 5556 324 sh (,) 5773 431 sh end MTsave restore pse gR gS 31 31 552 730 rC 97 245 :M f2_12 sf 2.604 .26(Each of the non-terminal symbols from the set )J 390 232 125 28 rC 390 260 :M f3_12 sf -.436( )A 515 260 :M psb currentpoint pse 390 232 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4000 div 896 3 -1 roll exch div scale currentpoint translate 64 45 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (\303) 87 264 sh 224 ns (,) 1688 467 sh ([) 922 743 sh (,) 1096 743 sh (]) 1349 743 sh (,) 3551 467 sh ([) 2729 743 sh (,) 2903 743 sh (]) 3102 743 sh 384 /Times-Italic f1 (V) -16 371 sh (Y) 1443 371 sh (Z) 3226 371 sh 224 ns (s) 185 467 sh (i) 1615 467 sh (s) 1762 467 sh (i) 716 743 sh (m) 1171 743 sh (j) 3472 467 sh (s) 3625 467 sh (j) 2517 743 sh (n) 2975 743 sh 384 /Symbol f1 (=) 407 371 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1578 /Symbol f3 ({) 1278 421 sh (}) 1875 421 sh 384 /Symbol f1 (\310) 2116 371 sh 384 1000 1664 /Symbol f3 ({) 3038 429 sh (}) 3738 429 sh 224 /Symbol f1 (\316) 796 743 sh (\316) 2603 743 sh 224 /Times-Roman f1 (1) 993 743 sh (1) 2800 743 sh 576 /MT-Extra f1 (U) 875 458 sh (U) 2635 458 sh end MTsave restore pse gR gS 31 31 552 730 rC 515 245 :M f2_12 sf 2.982 .298( may)J 97 275 :M .285 .028(appear at most once in any single production. When we consider composition in)J 97 293 :M 1.197 .12(Chapter\3124, this requirement will greatly simplify our ability to merge module)J 97 311 :M -.084(grammars.)A 97 341 :M .027 .003(As an example, all of the following are valid transaction productions according to)J 97 359 :M -.021(the above requirements:)A 259 375 125 62 rC 384 437 :M psb currentpoint pse 259 375 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4000 div 1984 3 -1 roll exch div scale currentpoint translate 64 45 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (T) 12 261 sh (Y) 1111 261 sh (Z) 1658 261 sh (Z) 2246 261 sh (T) 0 752 sh (Y) 1111 752 sh (Y) 1644 752 sh (Y) 2164 752 sh (Z) 2723 752 sh (Z) 3307 752 sh (T) 39 1243 sh (Z) 1134 1243 sh (Z) 1731 1243 sh (T) -12 1732 sh (Y) 1111 1732 sh 224 ns (s) 347 357 sh (s) 1445 357 sh (s) 2033 357 sh (s) 2657 357 sh (s) 374 848 sh (s) 1481 848 sh (s) 2001 848 sh (s) 2537 848 sh (s) 3121 848 sh (s) 3709 850 sh (s) 374 1339 sh (s) 1545 1339 sh (s) 2145 1339 sh (s) 359 1828 sh (s) 1472 1830 sh 224 /Times-Roman f1 (1) 170 357 sh (1) 1268 357 sh (1) 1856 357 sh (2) 2462 357 sh (4) 180 848 sh (2) 1286 848 sh (3) 1816 848 sh (4) 2343 848 sh (3) 2936 848 sh (5) 3522 850 sh (1) 197 1339 sh (2) 1350 1339 sh (4) 1951 1339 sh (2) 164 1828 sh (5) 1285 1830 sh 160 ns (0) 429 413 sh (0) 1527 413 sh (0) 2115 413 sh (0) 2739 413 sh (1) 442 904 sh (1) 1549 904 sh (1) 2069 904 sh (1) 2605 904 sh (1) 3189 904 sh (1) 3777 906 sh (1) 442 1395 sh (1) 1613 1395 sh (1) 2213 1395 sh (3) 437 1884 sh (3) 1550 1886 sh 224 /Times-Roman f1 (,) 273 357 sh (,) 1371 357 sh (,) 1959 357 sh (,) 2583 357 sh (,) 300 848 sh (,) 1407 848 sh (,) 1927 848 sh (,) 2463 848 sh (,) 3047 848 sh (,) 3635 850 sh (,) 300 1339 sh (,) 1471 1339 sh (,) 2071 1339 sh (,) 285 1828 sh (,) 1398 1830 sh 384 /Symbol f1 (\256) 647 261 sh (\256) 647 752 sh (\256) 647 1243 sh (\256) 647 1732 sh end MTsave restore pse gR gS 31 31 552 730 rC 97 464 :M f2_12 sf 4.336 .434(The complete set of productions for the basic grammar is formed by)J 97 470 136 15 rC 233 485 :M psb currentpoint pse 97 470 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4352 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 261 sh (BPA) 965 261 sh (BPB) 2226 261 sh (BPT) 3503 261 sh 224 ns (s) 415 357 sh (s) 1644 357 sh (s) 2905 357 sh (s) 4150 357 sh 384 /Symbol f1 (=) 637 261 sh (\310) 1839 261 sh (\310) 3116 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 233 480 :M f2_12 sf (.)S 97 510 :M f0_13 sf -.155(3.2.2)A 142 510 :M -.012(Prerequisite Relation)A 97 538 :M f2_12 sf .505 .05(The prerequisite relation )J 243 528 39 15 rC 282 543 :M psb currentpoint pse 243 528 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1248 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (prereq) 28 261 sh 224 ns (s) 1050 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 282 538 :M f2_12 sf .653 .065( is defined to indicate whether two events in a)J 97 556 :M 1.484 .148(module are temporally related. For example, if )J 381 545 78 16 rC 459 561 :M psb currentpoint pse 381 545 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2496 div 512 3 -1 roll exch div scale currentpoint translate 64 36 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -81 217 81 0 vb 16 th 81 217 0 217 vb 16 th 81 217 756 0 vb 16 th -81 217 837 217 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 96 316 sh (b) 501 316 sh 384 /Times-Roman f1 (,) 365 316 sh 384 /Symbol f1 (\316) 948 316 sh 384 /Times-Italic f1 (prereq) 1281 316 sh 224 ns (s) 2303 412 sh end MTsave restore pse gR gS 31 31 552 730 rC 459 556 :M f2_12 sf 1.64 .164(, then event )J 535 549 11 9 rC 546 558 :M psb currentpoint pse 535 549 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 352 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) -30 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 97 575 :M f2_12 sf -.013(must occur before event )A 232 565 10 14 rC 242 579 :M psb currentpoint pse 232 565 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 320 div 448 3 -1 roll exch div scale currentpoint translate 64 36 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) -5 284 sh end MTsave restore pse gR gS 31 31 552 730 rC 242 575 :M f2_12 sf -.024( can occur. We say that the occurrence of event )A 508 568 11 9 rC 519 577 :M psb currentpoint pse 508 568 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 352 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) -30 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 519 575 :M f2_12 sf -.069( \322is a)A 97 593 :M -.001(prerequisite for the occurrence of\323 event )A 322 583 10 14 rC 332 597 :M psb currentpoint pse 322 583 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 320 div 448 3 -1 roll exch div scale currentpoint translate 64 36 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) -5 284 sh end MTsave restore pse gR gS 31 31 552 730 rC 332 593 :M f2_12 sf (.)S 97 624 :M 1.546 .155(In the single module case, the prerequisite relation is analogous to a simple)J 97 642 :M 1.059 .106(connectivity matrix. Therefore, we can consider a directed graph in which the)J 97 660 :M .849 .085(vertices correspond to the terminal symbols, and a directed arc exists between)J 97 676 :M -.037(vertex )A 135 669 11 9 rC 146 678 :M psb currentpoint pse 135 669 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 352 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) -30 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 146 676 :M f2_12 sf -.071( and vertex )A 212 666 10 14 rC 222 680 :M psb currentpoint pse 212 666 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 320 div 448 3 -1 roll exch div scale currentpoint translate 64 36 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) -5 284 sh end MTsave restore pse gR gS 31 31 552 730 rC 222 676 :M f2_12 sf -.048( whenever )A 282 665 78 16 rC 360 681 :M psb currentpoint pse 282 665 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2496 div 512 3 -1 roll exch div scale currentpoint translate 64 36 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -81 217 81 0 vb 16 th 81 217 0 217 vb 16 th 81 217 756 0 vb 16 th -81 217 837 217 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 96 316 sh (b) 501 316 sh 384 /Times-Roman f1 (,) 365 316 sh 384 /Symbol f1 (\316) 948 316 sh 384 /Times-Italic f1 (prereq) 1281 316 sh 224 ns (s) 2303 412 sh end MTsave restore pse gR gS 31 31 552 730 rC 360 676 :M f2_12 sf (.)S endp %%Page: 109 109 %%BeginPageSetup initializepage (nestor; page: 109 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(38)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 169 94 9 15 rC 178 109 :M psb currentpoint pse 169 94 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (r) -9 261 sh 224 ns (s) 100 357 sh end MTsave restore pse gR gS 310 94 28 15 rC 338 109 :M psb currentpoint pse 310 94 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPB) 10 261 sh 224 ns (s) 689 357 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 91 1 1 135 90 @b -1 -1 136 91 1 1 135 90 @b 136 91 -1 1 211 90 1 136 90 @a -1 -1 212 91 1 1 211 90 @b 212 91 -1 1 436 90 1 212 90 @a -1 -1 437 91 1 1 436 90 @b -1 -1 437 91 1 1 436 90 @b -1 -1 136 109 1 1 135 91 @b -1 -1 212 109 1 1 211 91 @b -1 -1 437 109 1 1 436 91 @b 161 113 26 15 rC 187 128 :M psb currentpoint pse 161 113 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 832 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (0) 101 292 sh (0) 420 292 sh 384 /Times-Roman f1 (,) 288 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) -33 315 sh (]) 619 315 sh end MTsave restore pse gR gS 289 111 71 28 rC 289 139 :M f3_12 sf -.436( )A 360 139 :M psb currentpoint pse 289 111 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2272 div 896 3 -1 roll exch div scale currentpoint translate 64 58 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 743 358 sh 224 ns (k) 954 455 sh (s) 1146 455 sh (k) -3 730 sh (b) 494 730 sh 224 /Times-Roman f1 (,) 1072 455 sh (,) 422 730 sh 384 /Symbol f1 (\256) 1354 358 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1583 /Symbol f3 ({) 552 408 sh (}) 2002 408 sh 224 /Symbol f1 (\316) 122 730 sh 224 1000 1227 /Symbol f3 ([) 248 745 sh (]) 622 745 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (e) 1818 358 sh 224 /Times-Roman f1 (1) 319 730 sh 576 /MT-Extra f1 (U) 149 445 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 110 1 1 135 109 @b 136 110 -1 1 211 109 1 136 109 @a -1 -1 212 110 1 1 211 109 @b 212 110 -1 1 436 109 1 212 109 @a -1 -1 437 110 1 1 436 109 @b -1 -1 136 139 1 1 135 110 @b -1 -1 212 139 1 1 211 110 @b -1 -1 437 139 1 1 436 110 @b 162 143 24 15 rC 186 158 :M psb currentpoint pse 162 143 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 768 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (0) 101 292 sh (1) 387 292 sh 384 /Times-Roman f1 (,) 288 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) -33 315 sh (]) 555 315 sh end MTsave restore pse gR gS 280 141 88 34 rC 280 175 :M f3_12 sf -.436( )A 368 175 :M psb currentpoint pse 280 141 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2816 div 1088 3 -1 roll exch div scale currentpoint translate 64 49 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 943 293 sh (T) 2022 293 sh (B) 943 759 sh 224 ns (k) 1154 390 sh (s) 1346 390 sh (k) 2201 390 sh (s) 2393 390 sh (k) 1154 856 sh (s) 1346 856 sh (k) -3 931 sh (b) 494 931 sh 224 /Times-Roman f1 (,) 1272 390 sh (,) 2319 390 sh (,) 1272 856 sh (,) 422 931 sh 384 /Symbol f1 (\256) 1554 293 sh (\256) 1554 759 sh (\354) 736 355 sh (\355) 736 624 sh (\356) 736 894 sh (\374) 2530 355 sh (\375) 2530 624 sh (\376) 2530 894 sh 224 ns (\316) 122 931 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 224 1000 1227 /Symbol f3 ([) 248 946 sh (]) 622 946 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (e) 2018 759 sh 224 /Times-Roman f1 (1) 319 931 sh 576 /MT-Extra f1 (U) 149 646 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 140 1 1 135 139 @b 136 140 -1 1 211 139 1 136 139 @a -1 -1 212 140 1 1 211 139 @b 212 140 -1 1 436 139 1 212 139 @a -1 -1 437 140 1 1 436 139 @b -1 -1 136 175 1 1 135 140 @b -1 -1 212 175 1 1 211 140 @b -1 -1 437 175 1 1 436 140 @b 163 179 22 15 rC 185 194 :M psb currentpoint pse 163 179 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 704 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (1) 68 292 sh (1) 323 292 sh 384 /Times-Roman f1 (,) 224 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) -33 315 sh (]) 491 315 sh end MTsave restore pse gR gS 284 177 81 28 rC 284 205 :M f3_12 sf -.436( )A 365 205 :M psb currentpoint pse 284 177 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2592 div 896 3 -1 roll exch div scale currentpoint translate 64 58 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 743 358 sh (T) 1822 358 sh 224 ns (k) 954 455 sh (s) 1146 455 sh (k) 2001 455 sh (s) 2193 455 sh (k) -3 730 sh (b) 494 730 sh 224 /Times-Roman f1 (,) 1072 455 sh (,) 2119 455 sh (,) 422 730 sh 384 /Symbol f1 (\256) 1354 358 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1583 /Symbol f3 ({) 552 408 sh (}) 2306 408 sh 224 /Symbol f1 (\316) 122 730 sh 224 1000 1227 /Symbol f3 ([) 248 745 sh (]) 622 745 sh 224 /Times-Roman f1 (1) 319 730 sh 576 /MT-Extra f1 (U) 149 445 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 176 1 1 135 175 @b 136 176 -1 1 211 175 1 136 175 @a -1 -1 212 176 1 1 211 175 @b 212 176 -1 1 436 175 1 212 175 @a -1 -1 437 176 1 1 436 175 @b -1 -1 136 205 1 1 135 176 @b -1 -1 212 205 1 1 211 176 @b -1 -1 437 205 1 1 436 176 @b 162 209 24 15 rC 186 224 :M psb currentpoint pse 162 209 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 768 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (1) 68 292 sh (2) 354 292 sh 384 /Times-Roman f1 (,) 224 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) -33 315 sh (]) 553 315 sh end MTsave restore pse gR gS 273 207 103 34 rC 273 241 :M f3_12 sf -.436( )A 376 241 :M psb currentpoint pse 273 207 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3296 div 1088 3 -1 roll exch div scale currentpoint translate 64 49 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 943 293 sh (T) 2022 293 sh (B) 943 759 sh (T) 2022 759 sh (T) 2495 759 sh 224 ns (k) 1154 390 sh (s) 1346 390 sh (k) 2201 390 sh (s) 2393 390 sh (k) 1154 856 sh (s) 1346 856 sh (k) 2201 856 sh (s) 2393 856 sh (k) 2674 856 sh (s) 2866 856 sh (k) -3 931 sh (b) 494 931 sh 224 /Times-Roman f1 (,) 1272 390 sh (,) 2319 390 sh (,) 1272 856 sh (,) 2319 856 sh (,) 2792 856 sh (,) 422 931 sh 384 /Symbol f1 (\256) 1554 293 sh (\256) 1554 759 sh (\354) 736 355 sh (\355) 736 624 sh (\356) 736 894 sh (\374) 3003 355 sh (\375) 3003 624 sh (\376) 3003 894 sh 224 ns (\316) 122 931 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 224 1000 1227 /Symbol f3 ([) 248 946 sh (]) 622 946 sh 224 /Times-Roman f1 (1) 319 931 sh 576 /MT-Extra f1 (U) 149 646 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 206 1 1 135 205 @b 136 206 -1 1 211 205 1 136 205 @a -1 -1 212 206 1 1 211 205 @b 212 206 -1 1 436 205 1 212 205 @a -1 -1 437 206 1 1 436 205 @b -1 -1 136 241 1 1 135 206 @b -1 -1 212 241 1 1 211 206 @b -1 -1 437 241 1 1 436 206 @b 160 245 28 15 rC 188 260 :M psb currentpoint pse 160 245 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (0) 101 292 sh 384 /Times-Roman f1 (,) 288 292 sh 384 /Symbol f1 (\245) 420 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) -33 315 sh (]) 701 315 sh end MTsave restore pse gR gS 272 243 104 34 rC 272 277 :M f3_12 sf -.436( )A 376 277 :M psb currentpoint pse 272 243 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3328 div 1088 3 -1 roll exch div scale currentpoint translate 64 49 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 943 293 sh (T) 2022 293 sh (B) 2517 293 sh (B) 943 759 sh 224 ns (k) 1154 390 sh (s) 1346 390 sh (k) 2201 390 sh (s) 2393 390 sh (k) 2728 390 sh (s) 2920 390 sh (k) 1154 856 sh (s) 1346 856 sh (k) -3 931 sh (b) 494 931 sh 224 /Times-Roman f1 (,) 1272 390 sh (,) 2319 390 sh (,) 2846 390 sh (,) 1272 856 sh (,) 422 931 sh 384 /Symbol f1 (\256) 1554 293 sh (\256) 1554 759 sh (\354) 736 355 sh (\355) 736 624 sh (\356) 736 894 sh (\374) 3057 355 sh (\375) 3057 624 sh (\376) 3057 894 sh 224 ns (\316) 122 931 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 224 1000 1227 /Symbol f3 ([) 248 946 sh (]) 622 946 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (e) 2018 759 sh 224 /Times-Roman f1 (1) 319 931 sh 576 /MT-Extra f1 (U) 149 646 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 242 1 1 135 241 @b 136 242 -1 1 211 241 1 136 241 @a -1 -1 212 242 1 1 211 241 @b 212 242 -1 1 436 241 1 212 241 @a -1 -1 437 242 1 1 436 241 @b -1 -1 136 277 1 1 135 242 @b -1 -1 212 277 1 1 211 242 @b -1 -1 437 277 1 1 436 242 @b 161 281 26 15 rC 187 296 :M psb currentpoint pse 161 281 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 832 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (1) 68 292 sh 384 /Times-Roman f1 (,) 224 292 sh 384 /Symbol f1 (\245) 356 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) -33 315 sh (]) 637 315 sh end MTsave restore pse gR gS 272 279 104 34 rC 272 313 :M f3_12 sf -.436( )A 376 313 :M psb currentpoint pse 272 279 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3328 div 1088 3 -1 roll exch div scale currentpoint translate 64 49 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 943 293 sh (T) 2022 293 sh (B) 2517 293 sh (B) 943 759 sh (T) 2022 759 sh 224 ns (k) 1154 390 sh (s) 1346 390 sh (k) 2201 390 sh (s) 2393 390 sh (k) 2728 390 sh (s) 2920 390 sh (k) 1154 856 sh (s) 1346 856 sh (k) 2201 856 sh (s) 2393 856 sh (k) -3 931 sh (b) 494 931 sh 224 /Times-Roman f1 (,) 1272 390 sh (,) 2319 390 sh (,) 2846 390 sh (,) 1272 856 sh (,) 2319 856 sh (,) 422 931 sh 384 /Symbol f1 (\256) 1554 293 sh (\256) 1554 759 sh (\354) 736 355 sh (\355) 736 624 sh (\356) 736 894 sh (\374) 3057 355 sh (\375) 3057 624 sh (\376) 3057 894 sh 224 ns (\316) 122 931 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 224 1000 1227 /Symbol f3 ([) 248 946 sh (]) 622 946 sh 224 /Times-Roman f1 (1) 319 931 sh 576 /MT-Extra f1 (U) 149 646 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 278 1 1 135 277 @b 136 278 -1 1 211 277 1 136 277 @a -1 -1 212 278 1 1 211 277 @b 212 278 -1 1 436 277 1 212 277 @a -1 -1 437 278 1 1 436 277 @b -1 -1 136 313 1 1 135 278 @b -1 -1 212 313 1 1 211 278 @b -1 -1 437 313 1 1 436 278 @b 142 315 63 29 rC 205 344 :M psb currentpoint pse 142 315 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2016 div 928 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (i) 746 308 sh (j) 1033 308 sh (i) 571 756 sh (j) 1126 756 sh 384 /Times-Roman f1 (,) 851 308 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1322 /Symbol f3 ([) 619 341 sh (]) 1160 341 sh 384 /Symbol f1 (\243) 274 756 sh (\243) 772 756 sh (<) 1339 756 sh (\245) 1642 756 sh 384 /Times-Roman f1 (0) -9 756 sh end MTsave restore pse gR gS 222 315 205 98 rC 222 413 :M f3_12 sf -.436( )A 222 413 :M f2_12 sf -.668( )A 427 413 :M psb currentpoint pse 222 315 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 6560 div 3136 3 -1 roll exch div scale currentpoint translate 64 49 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 943 677 sh (T) 2022 677 sh (T) 2495 677 sh (T) 2968 677 sh (T) 3867 677 sh (B) 943 1527 sh (T) 2022 1527 sh (T) 2495 1527 sh (T) 2968 1527 sh (T) 3867 1527 sh (T) 4340 1527 sh (B) 943 2871 sh (T) 2022 2871 sh (T) 2495 2871 sh (T) 2968 2871 sh (T) 3867 2871 sh (T) 4340 2871 sh (T) 4813 2871 sh (T) 5286 2871 sh (T) 5759 2871 sh 224 ns (k) 1154 774 sh (s) 1346 774 sh (k) 2201 774 sh (s) 2393 774 sh (k) 2674 774 sh (s) 2866 774 sh (k) 3147 774 sh (s) 3339 774 sh (k) 4046 774 sh (s) 4238 774 sh (i) 2846 192 sh (k) 1154 1624 sh (s) 1346 1624 sh (k) 2201 1624 sh (s) 2393 1624 sh (k) 2674 1624 sh (s) 2866 1624 sh (k) 3147 1624 sh (s) 3339 1624 sh (k) 4046 1624 sh (s) 4238 1624 sh (k) 4519 1624 sh (s) 4711 1624 sh (i) 2946 1042 sh (k) 1154 2968 sh (s) 1346 2968 sh (k) 2201 2968 sh (s) 2393 2968 sh (k) 2674 2968 sh (s) 2866 2968 sh (k) 3147 2968 sh (s) 3339 2968 sh (k) 4046 2968 sh (s) 4238 2968 sh (k) 4519 2968 sh (s) 4711 2968 sh (k) 4992 2968 sh (s) 5184 2968 sh (k) 5465 2968 sh (s) 5657 2968 sh (k) 5938 2968 sh (s) 6130 2968 sh (j) 3808 2343 sh 224 /Times-Roman f1 (,) 1272 774 sh (,) 2319 774 sh (,) 2792 774 sh (,) 3265 774 sh (,) 4164 774 sh (,) 1272 1624 sh (,) 2319 1624 sh (,) 2792 1624 sh (,) 3265 1624 sh (,) 4164 1624 sh (,) 4637 1624 sh (,) 1272 2968 sh (,) 2319 2968 sh (,) 2792 2968 sh (,) 3265 2968 sh (,) 4164 2968 sh (,) 4637 2968 sh (,) 5110 2968 sh (,) 5583 2968 sh (,) 6056 2968 sh 384 /Symbol f1 (\256) 1554 677 sh (\256) 1554 1527 sh (\256) 1554 2871 sh 224 ns (+) 3034 1042 sh 384 /MT-Extra f1 (K) 3474 677 sh (6) 2034 306 sh (7) 2998 306 sh (4) 2402 306 sh (4) 2706 306 sh (8) 3970 306 sh (4) 3372 306 sh (4) 3745 306 sh (K) 3474 1527 sh (6) 2034 1156 sh (7) 3234 1156 sh (4) 2402 1156 sh (4) 2775 1156 sh (4) 2942 1156 sh (8) 4443 1156 sh (4) 3608 1156 sh (4) 3981 1156 sh (4) 4326 1156 sh (M) 1704 2024 sh (K) 3474 2871 sh (6) 2034 2500 sh (7) 3944 2500 sh (4) 2402 2500 sh (4) 2775 2500 sh (4) 3148 2500 sh 224 /NewCenturySchlbk-Roman f1 ( times) 2908 192 sh ( times) 3279 1042 sh ( times) 3870 2343 sh 224 /Times-Roman f1 (1) 3162 1042 sh 384 /MT-Extra f1 (4) 3521 2500 sh (4) 3521 2500 sh (4) 3652 2500 sh (8) 5862 2500 sh (4) 4318 2500 sh (4) 4691 2500 sh (4) 5064 2500 sh (4) 5437 2500 sh (4) 5745 2500 sh 576 ns (U) 149 1702 sh 384 /Symbol f1 (\354) 736 355 sh (\355) 736 1680 sh (\357) 736 726 sh (\357) 736 1099 sh (\357) 736 1388 sh (\356) 736 3006 sh (\357) 736 2054 sh (\357) 736 2427 sh (\357) 736 2800 sh (\374) 6267 355 sh (\375) 6267 1680 sh (\357) 6267 726 sh (\357) 6267 1099 sh (\357) 6267 1388 sh (\376) 6267 3006 sh (\357) 6267 2054 sh (\357) 6267 2427 sh (\357) 6267 2800 sh 224 ns (\316) 122 1987 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 224 1000 1227 /Symbol f3 ([) 248 2002 sh (]) 622 2002 sh 224 /Times-Italic f1 (k) -3 1987 sh (b) 494 1987 sh 224 /Times-Roman f1 (1) 319 1987 sh 224 /Times-Roman f1 (,) 422 1987 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 314 1 1 135 313 @b 136 314 -1 1 211 313 1 136 313 @a -1 -1 212 314 1 1 211 313 @b 212 314 -1 1 436 313 1 212 313 @a -1 -1 437 314 1 1 436 313 @b -1 -1 136 413 1 1 135 314 @b -1 -1 212 413 1 1 211 314 @b -1 -1 437 413 1 1 436 314 @b 152 415 43 26 rC 195 441 :M psb currentpoint pse 152 415 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1376 div 832 3 -1 roll exch div scale currentpoint translate 64 49 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (i) 369 292 sh (i) 571 724 sh 384 /Times-Roman f1 (,) 474 292 sh 384 /Symbol f1 (\245) 606 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) 242 315 sh (]) 887 315 sh 384 /Symbol f1 (\243) 274 724 sh (<) 774 724 sh 384 /Times-Roman f1 (0) -9 724 sh (2) 1075 724 sh end MTsave restore pse gR gS 272 415 104 42 rC 272 457 :M f3_12 sf -.436( )A 272 457 :M f2_12 sf -.668( )A 376 457 :M psb currentpoint pse 272 415 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3328 div 1344 3 -1 roll exch div scale currentpoint translate 64 34 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 943 293 sh (T) 2022 293 sh (B) 2517 293 sh (B) 943 1109 sh (T) 2124 1109 sh 224 ns (k) 1154 390 sh (s) 1346 390 sh (k) 2201 390 sh (s) 2393 390 sh (k) 2728 390 sh (s) 2920 390 sh (k) 1154 1206 sh (s) 1346 1206 sh (k) 2303 1206 sh (s) 2495 1206 sh (i) 2025 658 sh (k) -3 1106 sh (b) 494 1106 sh 224 /Times-Roman f1 (,) 1272 390 sh (,) 2319 390 sh (,) 2846 390 sh (,) 1272 1206 sh (,) 2421 1206 sh (,) 422 1106 sh 384 /Symbol f1 (\256) 1554 293 sh (\256) 1554 1109 sh (\354) 736 355 sh (\355) 736 799 sh (\357) 736 507 sh (\356) 736 1244 sh (\357) 736 1130 sh (\374) 3057 355 sh (\375) 3057 799 sh (\357) 3057 507 sh (\376) 3057 1244 sh (\357) 3057 1130 sh 224 ns (\316) 122 1106 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 224 1000 1227 /Symbol f3 ([) 248 1121 sh (]) 622 1121 sh 224 /NewCenturySchlbk-Roman f1 ( times) 2087 658 sh 384 1440 1000 /MT-Extra f3 (}) 2136 755 sh 576 /MT-Extra f1 (U) 149 821 sh 224 /Times-Roman f1 (1) 319 1106 sh end MTsave restore pse gR gS 31 31 552 730 rC -1 -1 136 414 1 1 135 413 @b 136 414 -1 1 211 413 1 136 413 @a -1 -1 212 414 1 1 211 413 @b 212 414 -1 1 436 413 1 212 413 @a -1 -1 437 414 1 1 436 413 @b -1 -1 136 457 1 1 135 414 @b -1 -1 136 458 1 1 135 457 @b -1 -1 136 458 1 1 135 457 @b 136 458 -1 1 211 457 1 136 457 @a -1 -1 212 457 1 1 211 414 @b -1 -1 212 458 1 1 211 457 @b 212 458 -1 1 436 457 1 212 457 @a -1 -1 437 457 1 1 436 414 @b -1 -1 437 458 1 1 436 457 @b -1 -1 437 458 1 1 436 457 @b 64 483 :M f2_12 sf .89 .089(The transaction production set )J 245 473 27 15 rC 272 488 :M psb currentpoint pse 245 473 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 864 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPT) 10 261 sh 224 ns (s) 657 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 272 483 :M f2_12 sf .947 .095( defines the derivations of the transaction)J 64 500 :M .943 .094(non-terminal symbols )J 193 490 17 16 rC 210 506 :M psb currentpoint pse 193 490 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (T) -12 261 sh 224 ns (k) 167 358 sh (s) 359 358 sh 224 /Times-Roman f1 (,) 285 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 210 500 :M f2_12 sf 1.181 .118(, representing the possible complete transactions for)J 64 521 :M -.045(block )A 96 511 9 12 rC 105 523 :M psb currentpoint pse 96 511 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 384 3 -1 roll exch div scale currentpoint translate 64 57 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (k) -6 263 sh end MTsave restore pse gR gS 31 31 552 730 rC 105 521 :M f2_12 sf .033 .003( of the module when in state )J 266 514 8 9 rC 274 523 :M psb currentpoint pse 266 514 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 274 521 :M f2_12 sf .026 .003(. The right hand side of each production in)J 64 538 :M .78 .078(the set )J 107 528 27 15 rC 134 543 :M psb currentpoint pse 107 528 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 864 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPT) 10 261 sh 224 ns (s) 657 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 134 538 :M f2_12 sf .772 .077( is a sequence of symbols from the set )J 355 525 125 28 rC 355 553 :M f3_12 sf -.436( )A 480 553 :M psb currentpoint pse 355 525 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4000 div 896 3 -1 roll exch div scale currentpoint translate 64 45 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (\303) 87 264 sh 224 ns (,) 1688 467 sh ([) 922 743 sh (,) 1096 743 sh (]) 1349 743 sh (,) 3551 467 sh ([) 2729 743 sh (,) 2903 743 sh (]) 3102 743 sh 384 /Times-Italic f1 (V) -16 371 sh (Y) 1443 371 sh (Z) 3226 371 sh 224 ns (s) 185 467 sh (i) 1615 467 sh (s) 1762 467 sh (i) 716 743 sh (m) 1171 743 sh (j) 3472 467 sh (s) 3625 467 sh (j) 2517 743 sh (n) 2975 743 sh 384 /Symbol f1 (=) 407 371 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1578 /Symbol f3 ({) 1278 421 sh (}) 1875 421 sh 384 /Symbol f1 (\310) 2116 371 sh 384 1000 1664 /Symbol f3 ({) 3038 429 sh (}) 3738 429 sh 224 /Symbol f1 (\316) 796 743 sh (\316) 2603 743 sh 224 /Times-Roman f1 (1) 993 743 sh (1) 2800 743 sh 576 /MT-Extra f1 (U) 875 458 sh (U) 2635 458 sh end MTsave restore pse gR gS 31 31 552 730 rC 480 538 :M f2_12 sf .146 .015(, with)J 64 568 :M -.029(the following restrictions:)A 206 565 :M f2_9 sf (43)S 64 598 :M f0_12 sf -.126(Requirement 3.1:)A 109 614 360 42 rC 109 656 :M f3_12 sf -.436( )A 109 656 :M f2_12 sf -.668( )A 469 656 :M psb currentpoint pse 109 614 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 11520 div 1344 3 -1 roll exch div scale currentpoint translate 64 50 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Symbol f1 (") -11 782 sh (\316) 497 782 sh (\316) 1431 782 sh ($) 3076 782 sh (\316) 3542 782 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1578 /Symbol f3 ({) 4581 832 sh (}) 5178 832 sh 384 /Symbol f1 (\346) 3832 479 sh (\350) 3832 1130 sh (\347) 3832 911 sh (\366) 5347 479 sh (\370) 5347 1130 sh (\367) 5347 911 sh (*) 5527 261 sh (\316) 6156 782 sh 384 1000 1664 /Symbol f3 ({) 7188 840 sh (}) 7888 840 sh 384 /Symbol f1 (\346) 6446 479 sh (\350) 6446 1130 sh (\347) 6446 911 sh (\366) 8057 479 sh (\370) 8057 1130 sh (\367) 8057 911 sh (*) 8237 261 sh 384 1000 1268 /Symbol f3 (\() 10170 801 sh (\)) 10538 801 sh 384 /Symbol f1 (=) 10752 782 sh 224 ns (\316) 4099 1154 sh 224 1000 1227 /Symbol f3 ([) 4225 1169 sh (]) 4652 1169 sh 224 /Symbol f1 (\316) 6752 1154 sh 224 1000 1227 /Symbol f3 ([) 6878 1169 sh (]) 7251 1169 sh 384 /Times-Italic f1 (s) 262 782 sh (S) 799 782 sh (p) 1158 782 sh (BPT) 1746 782 sh (y) 3286 782 sh (Y) 4746 782 sh (z) 5916 782 sh (Z) 7376 782 sh (rhs) 9680 782 sh (p) 10342 782 sh (yz) 11080 782 sh 224 ns (s) 2393 878 sh (i) 4918 878 sh (s) 5065 878 sh (i) 4019 1154 sh (m) 4474 1154 sh (j) 7622 878 sh (s) 7775 878 sh (j) 6666 1154 sh (n) 7124 1154 sh 384 /Times-Roman f1 (,) 989 782 sh (,) 2512 782 sh (,) 5727 782 sh 224 ns (,) 4991 878 sh (,) 4399 1154 sh (,) 7701 878 sh (,) 7052 1154 sh 224 /Times-Roman f1 (1) 4296 1154 sh (1) 6949 1154 sh 576 /MT-Extra f1 (U) 4178 869 sh (U) 6785 869 sh 384 /NewCenturySchlbk-Roman f1 (s.t.) 8797 782 sh end MTsave restore pse gR gS 31 31 552 730 rC -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 64 677.24 -.24 .24 207.24 677 .24 64 677 @a 64 696 :M f2_9 sf -.025(43)A f2_10 sf 0 3 rm -.026(The expression )A 0 -3 rm 146 684 16 16 rC 162 700 :M psb currentpoint pse 146 684 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 512 div 512 3 -1 roll exch div scale currentpoint translate 64 49 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (A) 17 431 sh 384 /Symbol f1 (*) 241 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 162 699 :M f2_10 sf -.021( indicates the Kleene closure of set )A 325 689 11 11 rC 336 700 :M psb currentpoint pse 325 689 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 352 div 352 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (A) 17 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 336 699 :M f2_10 sf (.)S endp %%Page: 110 110 %%BeginPageSetup initializepage (nestor; page: 110 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 97 64 :M f1_10 sf -.018(Modular Specification)A 533 64 :M f0_12 sf -.781(37)A 97 101 :M f2_12 sf .433 .043(set of )J f1_12 sf 1.457 .146(transaction productions)J 268 101 :M f2_12 sf 1.666 .167( )J 273 91 27 15 rC 300 106 :M psb currentpoint pse 273 91 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 864 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPT) 10 261 sh 224 ns (s) 657 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 300 101 :M f2_12 sf 1.366 .137(. The complete set of basic productions is)J 97 119 :M -.046(then constructed by )A 210 109 136 15 rC 346 124 :M psb currentpoint pse 210 109 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4352 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 261 sh (BPA) 965 261 sh (BPB) 2226 261 sh (BPT) 3503 261 sh 224 ns (s) 415 357 sh (s) 1644 357 sh (s) 2905 357 sh (s) 4150 357 sh 384 /Symbol f1 (=) 637 261 sh (\310) 1839 261 sh (\310) 3116 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 346 119 :M f2_12 sf (.)S 97 151 :M -.011(All modules include the following set of common productions:)A 166 167 312 28 rC 166 195 :M f3_12 sf -.436( )A 478 195 :M psb currentpoint pse 166 167 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 9984 div 896 3 -1 roll exch div scale currentpoint translate 64 45 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPA) 10 371 sh (A) 1405 371 sh (B) 2314 371 sh (B) 2805 371 sh (B) 3758 371 sh (Y) 5611 371 sh (Z) 8295 371 sh 224 ns (s) 689 467 sh (s) 1616 467 sh (s) 2681 467 sh (s) 3208 467 sh (b) 3967 467 sh (s) 4162 467 sh (i) 5783 467 sh (s) 5930 467 sh (i) 6855 467 sh (i) 4884 743 sh (m) 5339 743 sh (j) 8541 467 sh (s) 8694 467 sh (j) 9629 467 sh (j) 7586 743 sh (n) 8044 743 sh 384 /Symbol f1 (=) 911 371 sh (\256) 1824 371 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1578 /Symbol f3 ({) 1207 421 sh (}) 4275 421 sh 384 /Symbol f1 (\310) 4516 371 sh (\256) 6138 371 sh 384 1000 1578 /Symbol f3 ({) 5446 421 sh (}) 6944 421 sh 384 /Symbol f1 (\310) 7185 371 sh (\256) 8902 371 sh 384 1000 1664 /Symbol f3 ({) 8107 429 sh (}) 9724 429 sh 224 /Symbol f1 (\316) 4964 743 sh (\316) 7672 743 sh 224 /Times-Roman f1 (1) 2504 467 sh (2) 3013 467 sh (1) 5161 743 sh (1) 7869 743 sh 224 /Times-Roman f1 (,) 2607 467 sh (,) 3134 467 sh (,) 4088 467 sh (,) 5856 467 sh ([) 5090 743 sh (,) 5264 743 sh (]) 5517 743 sh (,) 8620 467 sh ([) 7798 743 sh (,) 7972 743 sh (]) 8171 743 sh 384 /MT-Extra f1 (K) 3343 371 sh 576 ns (U) 5043 458 sh (U) 7704 458 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 6588 371 sh (b) 9377 371 sh end MTsave restore pse gR gS 31 31 552 730 rC 97 220 :M f2_12 sf .139 .014(In the set )J 155 210 28 15 rC 183 225 :M psb currentpoint pse 155 210 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPA) 10 261 sh 224 ns (s) 689 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 183 220 :M f2_12 sf .129 .013(, the symbol )J 255 210 13 15 rC 268 225 :M psb currentpoint pse 255 210 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 416 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (A) 17 261 sh 224 ns (s) 228 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 268 220 :M f2_12 sf .244 .024( is the goal symbol for state )J 426 213 8 9 rC 434 222 :M psb currentpoint pse 426 213 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 434 220 :M f2_12 sf .228 .023(. It derives all valid)J 97 240 :M .004 0(event sequences for that state. We mentioned earlier that each input and output)J 97 258 :M 1.722 .172(event terminal symbol is associated with a particular state-specific input or)J 97 276 :M .459 .046(output non-terminal symbol. This relationship is achieved through productions)J 97 291 :M -.222(in )A 111 281 28 15 rC 139 296 :M psb currentpoint pse 111 281 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPA) 10 261 sh 224 ns (s) 689 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 139 291 :M f2_12 sf -.027( of the form )A 206 281 44 15 rC 250 296 :M psb currentpoint pse 206 281 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1408 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (Y) -16 261 sh 224 ns (i) 156 357 sh (s) 303 357 sh (i) 1228 357 sh 224 /Times-Roman f1 (,) 229 357 sh 384 /Symbol f1 (\256) 511 261 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 961 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 250 291 :M f2_12 sf -.141( and )A 278 281 47 16 rC 325 297 :M psb currentpoint pse 278 281 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1504 div 512 3 -1 roll exch div scale currentpoint translate 64 36 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (Z) 7 284 sh 224 ns (j) 253 380 sh (s) 406 380 sh (j) 1341 380 sh 224 /Times-Roman f1 (,) 332 380 sh 384 /Symbol f1 (\256) 614 284 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) 1089 284 sh end MTsave restore pse gR gS 31 31 552 730 rC 325 291 :M f2_12 sf -.016(, respectively.)A 97 321 :M 2.327 .233(The block non-terminals )J 248 311 19 16 rC 267 327 :M psb currentpoint pse 248 311 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 10 261 sh 224 ns (k) 221 358 sh (s) 413 358 sh 224 /Times-Roman f1 (,) 339 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 267 321 :M f2_12 sf 2.657 .266( are derived in terms of the transaction non)J 542 321 :M (-)S 97 339 :M .465 .046(terminals )J 156 329 17 16 rC 173 345 :M psb currentpoint pse 156 329 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (T) -12 261 sh 224 ns (k) 167 358 sh (s) 359 358 sh 224 /Times-Roman f1 (,) 285 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 173 339 :M f2_12 sf 1.048 .105( in the block production set )J 337 329 28 15 rC 365 344 :M psb currentpoint pse 337 329 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPB) 10 261 sh 224 ns (s) 689 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 365 339 :M f2_12 sf 1.008 .101(. Only three symbol types may)J 97 357 :M 1.005 .101(occur on the right-hand side of a )J 291 347 19 16 rC 310 363 :M psb currentpoint pse 291 347 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 10 261 sh 224 ns (k) 221 358 sh (s) 413 358 sh 224 /Times-Roman f1 (,) 339 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 310 357 :M f2_12 sf .996 .1( production: one or more )J 461 347 17 16 rC 478 363 :M psb currentpoint pse 461 347 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (T) -12 261 sh 224 ns (k) 167 358 sh (s) 359 358 sh 224 /Times-Roman f1 (,) 285 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 478 357 :M f2_12 sf .96 .096( symbols, at)J 97 375 :M .753 .075(most one )J 153 365 19 16 rC 172 381 :M psb currentpoint pse 153 365 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 10 261 sh 224 ns (k) 221 358 sh (s) 413 358 sh 224 /Times-Roman f1 (,) 339 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 172 375 :M f2_12 sf .854 .085( symbol, or the empty string symbol )J 384 368 9 9 rC 393 377 :M psb currentpoint pse 384 368 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (e) -16 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 393 375 :M f2_12 sf .952 .095( . The structure of the set)J 97 384 28 15 rC 125 399 :M psb currentpoint pse 97 384 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPB) 10 261 sh 224 ns (s) 689 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 125 394 :M f2_12 sf -.041( depends on the set )A 235 384 9 15 rC 244 399 :M psb currentpoint pse 235 384 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (r) -9 261 sh 224 ns (s) 100 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 244 394 :M f2_12 sf -.003(. The following table provides some common cases:)A f2_9 sf 0 -3 rm (42)S 0 3 rm -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 97 667.24 -.24 .24 240.24 667 .24 97 667 @a 97 682 :M (42)S f2_10 sf 0 3 rm -.005(The case where )A 0 -3 rm 182 674 46 16 rC 228 690 :M psb currentpoint pse 182 674 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1472 div 512 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (r) -9 292 sh (i) 734 292 sh 224 ns (s) 100 388 sh 384 /Symbol f1 (=) 322 292 sh (\245) 971 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) 607 315 sh (]) 1252 315 sh 384 /Times-Roman f1 (,) 839 292 sh end MTsave restore pse gR gS 31 31 552 730 rC 228 685 :M f2_10 sf -.097( with )A 255 675 24 12 rC 279 687 :M psb currentpoint pse 255 675 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 768 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (i) -16 261 sh 384 /Symbol f1 (\263) 185 261 sh 384 /Times-Roman f1 (2) 487 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 279 685 :M f2_10 sf .101 .01( is not included in the table. Basic production sets can be)J 97 699 :M -.001(easily constructed for this case, but additional non-terminal symbols are required.)A endp %%Page: 111 111 %%BeginPageSetup initializepage (nestor; page: 111 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(36)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 64 101 :M f2_12 sf .603 .06(The production set )J 175 91 12 15 rC 187 106 :M psb currentpoint pse 175 91 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (P) 6 261 sh 224 ns (s) 177 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 187 101 :M f2_12 sf .71 .071( will be presented in three distinct components: the basic)J 64 119 :M .46 .046(production set )J 148 109 19 15 rC 167 124 :M psb currentpoint pse 148 109 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 261 sh 224 ns (s) 415 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 167 119 :M f2_12 sf .584 .058(, the delay production set )J 316 109 20 15 rC 336 124 :M psb currentpoint pse 316 109 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 640 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (DP) 10 261 sh 224 ns (s) 458 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 336 119 :M f2_12 sf .536 .054(, and the shuffle production set)J 64 127 17 15 rC 81 142 :M psb currentpoint pse 64 127 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (SP) -3 261 sh 224 ns (s) 360 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 81 137 :M f2_12 sf .157 .016(. It is possible to specify )J 222 127 12 15 rC 234 142 :M psb currentpoint pse 222 127 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 384 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (P) 6 261 sh 224 ns (s) 177 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 234 137 :M f2_12 sf .18 .018( directly, but having the set of productions broken)J 64 157 :M 1.319 .132(into components will simplify the description of the composition algorithm in)J 64 175 :M .074 .007(Section\3124.2. Intuitively, having separate components also simplifies the analysis)J 64 193 :M -.015(and verification of the more complex modules.)A 64 223 :M 2.042 .204(Once we have developed each of the three components, the complete set of)J 64 241 :M -.013(productions for a particular module in state )A 310 234 8 9 rC 318 243 :M psb currentpoint pse 310 234 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 318 241 :M f2_12 sf -.052( is constructed by)A 415 238 :M f2_9 sf (41)S 236 258 103 15 rC 339 273 :M psb currentpoint pse 236 258 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3296 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (P) 6 261 sh (BP) 727 261 sh (DP) 1714 261 sh (SP) 2731 261 sh 224 ns (s) 177 357 sh (s) 1132 357 sh (s) 2162 357 sh (s) 3094 357 sh 384 /Symbol f1 (=) 399 261 sh (\310) 1327 261 sh (\310) 2357 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 339 272 :M f2_12 sf (.)S 64 299 :M f0_13 sf -.155(3.2.1)A 109 299 :M -.015(Basic Production Set)A 64 327 :M f2_12 sf .255 .026(The )J 90 327 :M f1_12 sf .833 .083(basic productions)J f2_12 sf .28 .028( \(in the set )J 254 317 19 15 rC 273 332 :M psb currentpoint pse 254 317 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 261 sh 224 ns (s) 415 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 273 327 :M f2_12 sf .638 .064(\) form a starting point in the grammatical)J 64 347 :M .524 .052(development. They do not account for possible time-delay or reordering effects.)J 64 365 :M 3.383 .338(The basic productions result in a language in which input event\(s\) are)J 64 383 :M -.013(immediately followed by their corresponding output event\(s\).)A 64 410 :M 2.715 .272(As mentioned above, the non-terminal symbol )J 351 400 17 16 rC 368 416 :M psb currentpoint pse 351 400 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (T) -12 261 sh 224 ns (k) 167 358 sh (s) 359 358 sh 224 /Times-Roman f1 (,) 285 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 368 410 :M f2_12 sf 2.91 .291( will represent a single)J 64 431 :M .825 .083(complete transaction for block )J 240 421 9 12 rC 249 433 :M psb currentpoint pse 240 421 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 384 3 -1 roll exch div scale currentpoint translate 64 57 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (k) -6 263 sh end MTsave restore pse gR gS 31 31 552 730 rC 249 431 :M f2_12 sf 1.108 .111( in state )J 302 424 8 9 rC 310 433 :M psb currentpoint pse 302 424 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 310 431 :M f2_12 sf .937 .094(. A particular block and state may)J 64 449 :M .338 .034(have one or more possible transaction types, each corresponding to a production)J 64 464 :M -.222(in )A 78 454 19 15 rC 97 469 :M psb currentpoint pse 78 454 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 261 sh 224 ns (s) 415 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 97 464 :M f2_12 sf -.027( with the non-terminal symbol )A 269 454 17 16 rC 286 470 :M psb currentpoint pse 269 454 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (T) -12 261 sh 224 ns (k) 167 358 sh (s) 359 358 sh 224 /Times-Roman f1 (,) 285 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 286 464 :M f2_12 sf -.04( on the left-hand side.)A 64 497 :M .327 .033(Having individual transactions clearly identified with a particular non-terminal)J 64 512 :M 2.43 .243(\(i.e., )J 95 502 17 16 rC 112 518 :M psb currentpoint pse 95 502 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (T) -12 261 sh 224 ns (k) 167 358 sh (s) 359 358 sh 224 /Times-Roman f1 (,) 285 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 112 512 :M f2_12 sf 2.401 .24(\) provides a convenient mechanism for examining the relationship)J 64 533 :M -.004(between the inputs and the outputs in a particular \(causally related\) collection of)A 64 551 :M .763 .076(events. This is probably the most important reason for using the grammatical)J 64 569 :M 1.142 .114(approach to represent event sequences, and will be further explored when we)J 64 587 :M -.024(consider properties in Chapter\3125.)A 64 615 :M .367 .037(We will develop the set of basic productions )J 313 605 19 15 rC 332 620 :M psb currentpoint pse 313 605 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 261 sh 224 ns (s) 415 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 332 615 :M f2_12 sf .314 .031( in three parts, corresponding to)J 64 633 :M .444 .044(the set of )J 121 633 :M f1_12 sf .436 .044(common productions)J f2_12 sf ( )S 240 623 28 15 rC 268 638 :M psb currentpoint pse 240 623 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPA) 10 261 sh 224 ns (s) 689 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 268 633 :M f2_12 sf .22 .022(, the set of )J f1_12 sf .715 .071(block productions)J 430 633 :M f2_12 sf .666 .067( )J 435 623 28 15 rC 463 638 :M psb currentpoint pse 435 623 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 896 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BPB) 10 261 sh 224 ns (s) 689 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 463 633 :M f2_12 sf .394 .039(, and the)J -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 64 680.24 -.24 .24 207.24 680 .24 64 680 @a 64 694 :M f2_9 sf -.056(41)A f2_10 sf 0 3 rm -.057(Obviously, )A 0 -3 rm 126 687 74 15 rC 200 702 :M psb currentpoint pse 126 687 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2368 div 480 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 276 sh (DP) 997 276 sh 224 ns (s) 415 372 sh (s) 1445 372 sh 384 /Symbol f1 (\307) 610 276 sh (=) 1667 276 sh (\306) 1971 276 sh end MTsave restore pse gR gS 31 31 552 730 rC 200 697 :M f2_10 sf -.557(, )A 206 687 73 15 rC 279 702 :M psb currentpoint pse 206 687 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2336 div 480 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (DP) 10 276 sh (SP) 1027 276 sh 224 ns (s) 458 372 sh (s) 1390 372 sh 384 /Symbol f1 (\307) 653 276 sh (=) 1612 276 sh (\306) 1916 276 sh end MTsave restore pse gR gS 31 31 552 730 rC 279 697 :M f2_10 sf -.149(, and )A 305 687 71 15 rC 376 702 :M psb currentpoint pse 305 687 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2272 div 480 3 -1 roll exch div scale currentpoint translate 64 44 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (BP) 10 276 sh (SP) 984 276 sh 224 ns (s) 415 372 sh (s) 1347 372 sh 384 /Symbol f1 (\307) 610 276 sh (=) 1569 276 sh (\306) 1873 276 sh end MTsave restore pse gR gS 31 31 552 730 rC 376 697 :M f2_10 sf (.)S endp %%Page: 112 112 %%BeginPageSetup initializepage (nestor; page: 112 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 97 64 :M f1_10 sf -.018(Modular Specification)A 533 64 :M f0_12 sf -.781(35)A 97 107 :M f2_12 sf (\245)S 115 91 50 16 rC 165 107 :M psb currentpoint pse 115 91 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1600 div 512 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (r) -9 292 sh 224 ns (s) 100 388 sh 384 /Symbol f1 (\315) 312 292 sh (\245) 1108 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1223 /Symbol f3 ([) 655 315 sh (]) 1389 315 sh 384 /Times-Roman f1 (0) 789 292 sh 384 /Times-Roman f1 (,) 976 292 sh end MTsave restore pse gR gS 31 31 552 730 rC 165 102 :M f2_12 sf 2.059 .206( an interval that defines the range of possible number of times)J 115 122 :M 1.199 .12(complete transactions may occur in state )J 357 115 8 9 rC 365 124 :M psb currentpoint pse 357 115 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 365 122 :M f2_12 sf 1.652 .165(. If )J 393 112 24 15 rC 417 127 :M psb currentpoint pse 393 112 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 768 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (i) -16 261 sh (r) 475 261 sh 224 ns (s) 584 357 sh 384 /Symbol f1 (\316) 179 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 417 122 :M f2_12 sf 1.397 .14(, then a sequence of )J 540 113 6 11 rC 546 124 :M psb currentpoint pse 540 113 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 192 div 352 3 -1 roll exch div scale currentpoint translate 64 27 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (i) -16 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 115 142 :M f2_12 sf -.006(complete transactions is a valid event sequence for state )A 430 135 8 9 rC 438 144 :M psb currentpoint pse 430 135 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 438 142 :M f2_12 sf (.)S 97 175 :M (\245)S 115 158 87 18 rC 202 176 :M psb currentpoint pse 115 158 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2784 div 576 3 -1 roll exch div scale currentpoint translate 64 55 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -84 230 877 0 vb 16 th 84 230 793 230 vb 16 th 84 230 2560 0 vb 16 th -84 230 2644 230 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (G) -11 329 sh (V) 906 329 sh (E) 1373 329 sh (P) 1758 329 sh (A) 2206 329 sh 224 ns (s) 253 425 sh (s) 1107 425 sh (s) 1929 425 sh (s) 2417 425 sh 384 /Symbol f1 (=) 475 329 sh 384 /Times-Roman f1 (,) 1226 329 sh (,) 1611 329 sh (,) 2048 329 sh end MTsave restore pse gR gS 31 31 552 730 rC 202 170 :M f2_12 sf ( the grammar describing the possible event sequences in state)S 115 180 26 12 rC 141 192 :M psb currentpoint pse 115 180 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 832 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh (S) 531 261 sh 384 /Symbol f1 (\316) 229 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 141 190 :M f2_12 sf .827 .083(. The sentences in the language )J 331 178 30 18 rC 361 196 :M psb currentpoint pse 331 178 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 960 div 576 3 -1 roll exch div scale currentpoint translate 64 56 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (L) 12 328 sh (G) 359 328 sh 224 ns (s) 623 424 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1388 /Symbol f3 (\() 226 358 sh (\)) 755 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 361 190 :M f2_12 sf .798 .08( will be all possible sequences of)J 115 211 :M -.01(events that are valid behaviours for the module while in state )A 461 204 8 9 rC 469 213 :M psb currentpoint pse 461 204 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 469 211 :M f2_12 sf (.)S 97 241 :M .311 .031(The non-terminal set )J 219 232 11 10 rC 230 242 :M psb currentpoint pse 219 232 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 352 div 320 3 -1 roll exch div scale currentpoint translate 64 27 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (E) 6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 230 241 :M f2_12 sf .33 .033( corresponds to the set of possible events and is common)J 97 259 :M 1.394 .139(to all state grammars. We will now define the remaining components of the)J 97 275 :M -.017(grammar )A 152 263 87 18 rC 239 281 :M psb currentpoint pse 152 263 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2784 div 576 3 -1 roll exch div scale currentpoint translate 64 55 translate /thick 0 def /th { dup setlinewidth /thick exch def } def 16 th /stb { newpath moveto 0 setlinewidth 2 copy rlineto } def /enb { rlineto neg exch neg exch rlineto closepath fill } def /hb { stb 0 thick enb } def /vb { stb thick 0 enb } def -84 230 877 0 vb 16 th 84 230 793 230 vb 16 th 84 230 2560 0 vb 16 th -84 230 2644 230 vb /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (G) -11 329 sh (V) 906 329 sh (E) 1373 329 sh (P) 1758 329 sh (A) 2206 329 sh 224 ns (s) 253 425 sh (s) 1107 425 sh (s) 1929 425 sh (s) 2417 425 sh 384 /Symbol f1 (=) 475 329 sh 384 /Times-Roman f1 (,) 1226 329 sh (,) 1611 329 sh (,) 2048 329 sh end MTsave restore pse gR gS 31 31 552 730 rC 239 275 :M f2_12 sf -.005( for a particular state\312)A 361 268 8 9 rC 369 277 :M psb currentpoint pse 361 268 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 369 275 :M f2_12 sf (.)S 97 306 :M .16 .016(For each input event terminal symbol )J 311 296 13 15 rC 324 311 :M psb currentpoint pse 311 296 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 416 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate -15 261 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) show 251 357 moveto 224 /Times-Italic f1 (i) show end pse gR gS 31 31 552 730 rC 324 306 :M f2_12 sf .112 .011( and each output event terminal symbol)J 97 313 13 16 rC 110 329 :M psb currentpoint pse 97 313 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 416 div 512 3 -1 roll exch div scale currentpoint translate 64 36 translate -23 284 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) show 237 380 moveto 224 /Times-Italic f1 (j) show end pse gR gS 31 31 552 730 rC 110 323 :M f2_12 sf .337 .034(, we define corresponding non-terminal symbols )J 382 313 16 15 rC 398 328 :M psb currentpoint pse 382 313 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 512 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (Y) -16 261 sh 224 ns (i) 156 357 sh (s) 303 357 sh 224 /Times-Roman f1 (,) 229 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 398 323 :M f2_12 sf .182 .018( and )J 427 313 19 16 rC 446 329 :M psb currentpoint pse 427 313 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (Z) 7 261 sh 224 ns (j) 253 357 sh (s) 406 357 sh 224 /Times-Roman f1 (,) 332 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 446 323 :M f2_12 sf .39 .039(. While the event)J 97 344 :M 2.653 .265(terminal symbols are common to all states, the corresponding event non-)J 97 362 :M .199 .02(terminal symbols are state-specific, as denoted by the additional state subscript.)J 97 380 :M .174 .017(The input and output non-terminals are state specific so that we can restrict the)J 97 398 :M -.005(intermixing of events to within a single state.)A 97 427 :M -.007(We then define )A 185 414 125 28 rC 185 442 :M f3_12 sf -.436( )A 310 442 :M psb currentpoint pse 185 414 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4000 div 896 3 -1 roll exch div scale currentpoint translate 64 45 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Roman f1 (\303) 87 264 sh 224 ns (,) 1688 467 sh ([) 922 743 sh (,) 1096 743 sh (]) 1349 743 sh (,) 3551 467 sh ([) 2729 743 sh (,) 2903 743 sh (]) 3102 743 sh 384 /Times-Italic f1 (V) -16 371 sh (Y) 1443 371 sh (Z) 3226 371 sh 224 ns (s) 185 467 sh (i) 1615 467 sh (s) 1762 467 sh (i) 716 743 sh (m) 1171 743 sh (j) 3472 467 sh (s) 3625 467 sh (j) 2517 743 sh (n) 2975 743 sh 384 /Symbol f1 (=) 407 371 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1578 /Symbol f3 ({) 1278 421 sh (}) 1875 421 sh 384 /Symbol f1 (\310) 2116 371 sh 384 1000 1664 /Symbol f3 ({) 3038 429 sh (}) 3738 429 sh 224 /Symbol f1 (\316) 796 743 sh (\316) 2603 743 sh 224 /Times-Roman f1 (1) 993 743 sh (1) 2800 743 sh 576 /MT-Extra f1 (U) 875 458 sh (U) 2635 458 sh end MTsave restore pse gR gS 31 31 552 730 rC 310 427 :M f2_12 sf .099 .01( to be the complete set of input and output)J 97 457 :M -.026(non-terminal symbols for state )A 271 450 8 9 rC 279 459 :M psb currentpoint pse 271 450 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 279 457 :M f2_12 sf (.)S 97 484 :M .101 .01(For each block )J 181 474 27 12 rC 208 486 :M psb currentpoint pse 181 474 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 864 div 384 3 -1 roll exch div scale currentpoint translate 64 57 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (k) -6 263 sh (b) 561 263 sh 384 /Symbol f1 (\316) 265 263 sh end MTsave restore pse gR gS 31 31 552 730 rC 208 484 :M f2_12 sf .092 .009( of the module, we define the block non-terminal symbol )J 524 474 19 16 rC 543 490 :M psb currentpoint pse 524 474 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 10 261 sh 224 ns (k) 221 358 sh (s) 413 358 sh 224 /Times-Roman f1 (,) 339 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 543 484 :M f2_12 sf (.)S 97 502 :M -.021(In the grammatical specification, a block non-terminal )A 402 492 19 16 rC 421 508 :M psb currentpoint pse 402 492 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 608 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (B) 10 261 sh 224 ns (k) 221 358 sh (s) 413 358 sh 224 /Times-Roman f1 (,) 339 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 421 502 :M f2_12 sf -.025( derives all valid event)A 97 523 :M .411 .041(sequences for block )J 210 513 9 12 rC 219 525 :M psb currentpoint pse 210 513 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 384 3 -1 roll exch div scale currentpoint translate 64 57 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (k) -6 263 sh end MTsave restore pse gR gS 31 31 552 730 rC 219 523 :M f2_12 sf .595 .059( in state )J 271 516 8 9 rC 279 525 :M psb currentpoint pse 271 516 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 279 523 :M f2_12 sf .6 .06(. These valid event sequences are sequences of)J 97 541 :M 1.03 .103(complete transactions. In the grammatical specification, the transaction non)J 542 541 :M (-)S 97 556 :M 2.28 .228(terminal symbol )J 200 546 17 16 rC 217 562 :M psb currentpoint pse 200 546 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 544 div 512 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (T) -12 261 sh 224 ns (k) 167 358 sh (s) 359 358 sh 224 /Times-Roman f1 (,) 285 358 sh end MTsave restore pse gR gS 31 31 552 730 rC 217 556 :M f2_12 sf 2.808 .281( derives a valid event sequence for a single complete)J 97 577 :M -.026(transaction for block )A 215 567 9 12 rC 224 579 :M psb currentpoint pse 215 567 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 384 3 -1 roll exch div scale currentpoint translate 64 57 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (k) -6 263 sh end MTsave restore pse gR gS 31 31 552 730 rC 224 577 :M f2_12 sf -.076( in state )A 273 570 8 9 rC 281 579 :M psb currentpoint pse 273 570 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 281 577 :M f2_12 sf (.)S 97 605 :M .032 .003(The non-terminal )J 198 595 13 15 rC 211 610 :M psb currentpoint pse 198 595 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 416 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (A) 17 261 sh 224 ns (s) 228 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 211 605 :M f2_12 sf .02 .002( is the start symbol for grammar )J 396 595 14 15 rC 410 610 :M psb currentpoint pse 396 595 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 448 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (G) -11 261 sh 224 ns (s) 253 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 410 605 :M f2_12 sf (, and derives all possible)S 97 625 :M -.031(event sequences for the module in state )A 319 618 8 9 rC 327 627 :M psb currentpoint pse 319 618 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 327 625 :M f2_12 sf -.02(. The complete non-terminal set for the)A 97 642 :M -.017(grammar )A 152 632 14 15 rC 166 647 :M psb currentpoint pse 152 632 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 448 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (G) -11 261 sh 224 ns (s) 253 357 sh end MTsave restore pse gR gS 31 31 552 730 rC 166 642 :M f2_12 sf -.048( is defined by )A 243 629 147 27 rC 243 656 :M f3_12 sf -.436( )A 390 656 :M psb currentpoint pse 243 629 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4704 div 864 3 -1 roll exch div scale currentpoint translate 64 51 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (V) -16 365 sh (A) 901 365 sh (B) 2586 365 sh (T) 3237 365 sh (V) 4323 365 sh 224 ns (s) 185 461 sh (s) 1112 461 sh (k) 2797 462 sh (s) 2989 462 sh (k) 3416 462 sh (s) 3608 462 sh (k) 1840 737 sh (b) 2337 737 sh (s) 4524 461 sh 384 /Symbol f1 (=) 407 365 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1401 /Symbol f3 ({) 703 398 sh (}) 1225 398 sh 384 /Symbol f1 (\310) 1466 365 sh 384 1000 1583 /Symbol f3 ({) 2395 415 sh (}) 3721 415 sh 384 /Symbol f1 (\310) 3962 365 sh 224 ns (\316) 1965 737 sh 224 /Times-Roman f1 (,) 2915 462 sh (,) 3534 462 sh ([) 2091 737 sh (,) 2265 737 sh (]) 2465 737 sh 384 ns (,) 3108 365 sh (\303) 4426 258 sh 224 /Times-Roman f1 (1) 2162 737 sh 576 /MT-Extra f1 (U) 1992 452 sh end MTsave restore pse gR gS 31 31 552 730 rC 390 642 :M f2_12 sf (.)S endp %%Page: 113 113 %%BeginPageSetup initializepage (nestor; page: 113 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(34)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 64 100 :M f2_12 sf .343 .034(Although we consider the module to be the smallest, stand-alone element in our)J 64 118 :M .192 .019(modelling methodology, it is necessary to maintain a module\325s block structure in)J 64 136 :M .206 .021(order to allow composition with other modules. This will be further described in)J 64 154 :M -.002(Section\3124.2 when the composition procedure is introduced.)A 64 184 :M 3.266 .327(We will now proceed to formally define all of the above concepts. The)J 64 202 :M 1.675 .167(presentation of the module specification will occur in two stages. First, the)J 64 220 :M 2.516 .252(structure for a particular state will be introduced. Next, the single-state)J 64 238 :M .655 .066(representation will be brought together under a global structure that describes)J 64 256 :M -.006(the behaviour of the module as it moves between different states.)A 64 285 :M 1.532 .153(Let )J 89 274 100 15 rC 89 289 :M f3_12 sf -.436( )A 189 289 :M psb currentpoint pse 89 274 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 3200 div 480 3 -1 roll exch div scale currentpoint translate 64 60 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (m) -4 292 sh (n) 402 292 sh (b) 719 292 sh 384 /Times-Roman f1 (,) 269 292 sh (,) 587 292 sh (,) 1638 292 sh (,) 1893 292 sh (,) 2210 292 sh (,) 2505 292 sh 384 /Symbol f1 (\316) 996 292 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1182 /Symbol f3 ({) 1279 305 sh (}) 2943 305 sh 384 /Times-Roman f1 (0) 1451 292 sh (1) 1737 292 sh (2) 2023 292 sh (3) 2335 292 sh 384 /MT-Extra f1 (K) 2603 292 sh end MTsave restore pse gR gS 31 31 552 730 rC 189 285 :M f2_12 sf 1.638 .164( be the number of module inputs, module outputs, and)J 64 304 :M 1.032 .103(blocks, respectively. We require that )J 283 294 48 12 rC 331 306 :M psb currentpoint pse 283 294 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 1536 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (b) -9 261 sh (m) 583 261 sh (n) 1238 261 sh 384 /Symbol f1 (\243) 274 261 sh (+) 944 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 331 304 :M f2_12 sf 1.159 .116(, since each block must have at)J 64 322 :M -.005(least one input or one output associated with it.)A f2_9 sf 0 -3 rm (40)S 0 3 rm 64 350 :M f2_12 sf 1.573 .157(For a module, define the terminal symbol )J 314 340 13 15 rC 327 355 :M psb currentpoint pse 314 340 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 416 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate -15 261 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) show 251 357 moveto 224 /Times-Italic f1 (i) show end pse gR gS 31 31 552 730 rC 327 350 :M f2_12 sf 1.588 .159( to correspond to a single input)J 64 367 :M .713 .071(event on stream )J 165 358 6 11 rC 171 369 :M psb currentpoint pse 165 358 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 192 div 352 3 -1 roll exch div scale currentpoint translate 64 27 translate -16 261 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def 384 /Times-Italic f1 (i) show end pse gR gS 31 31 552 730 rC 171 367 :M f2_12 sf .599 .06( and )J 201 357 13 16 rC 214 373 :M psb currentpoint pse 201 357 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 416 div 512 3 -1 roll exch div scale currentpoint translate 64 36 translate -23 284 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) show 237 380 moveto 224 /Times-Italic f1 (j) show end pse gR gS 31 31 552 730 rC 214 367 :M f2_12 sf .732 .073( to refer to a single output event on stream )J 466 358 8 13 rC 474 371 :M psb currentpoint pse 466 358 :M psb 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 416 3 -1 roll exch div scale currentpoint translate 64 27 translate 41 261 moveto /fs 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def 384 /Times-Italic f1 (j) show end pse gR gS 31 31 552 730 rC 474 367 :M f2_12 sf .77 .077(. Each)J 64 388 :M .206 .021(input and output stream is assigned a particular event symbol, corresponding to)J 64 405 :M .215 .021(the subscript on the event symbol. We then define )J 351 393 66 27 rC 351 420 :M f3_12 sf -.436( )A 417 420 :M psb currentpoint pse 351 393 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2112 div 864 3 -1 roll exch div scale currentpoint translate 32 38 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 224 /Times-Italic f1 (I) 85 176 sh (i) 1780 442 sh (i) 800 718 sh (m) 1255 718 sh 384 ns (E) 150 346 sh 384 /Symbol f1 (=) 491 346 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1395 /Symbol f3 ({) 1362 379 sh (}) 1869 379 sh 224 /Symbol f1 (\316) 880 718 sh 224 1000 1227 /Symbol f3 ([) 1006 733 sh (]) 1433 733 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 1513 346 sh 224 /Times-Roman f1 (1) 1077 718 sh 224 /Times-Roman f1 (,) 1180 718 sh 576 /MT-Extra f1 (U) 959 433 sh end MTsave restore pse gR gS 31 31 552 730 rC 417 405 :M f2_12 sf .182 .018( and )J 445 392 68 28 rC 445 420 :M f3_12 sf -.436( )A 513 420 :M psb currentpoint pse 445 392 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2176 div 896 3 -1 roll exch div scale currentpoint translate 32 45 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 224 /Times-Italic f1 (O) 71 201 sh (j) 1841 467 sh (j) 891 743 sh (n) 1349 743 sh 384 ns (E) 208 371 sh 384 /Symbol f1 (=) 549 371 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1664 /Symbol f3 ({) 1413 429 sh (}) 1936 429 sh 224 /Symbol f1 (\316) 977 743 sh 224 1000 1227 /Symbol f3 ([) 1103 758 sh (]) 1476 758 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (b) 1589 371 sh 224 /Times-Roman f1 (1) 1174 743 sh 224 /Times-Roman f1 (,) 1277 743 sh 576 /MT-Extra f1 (U) 1010 458 sh end MTsave restore pse gR gS 31 31 552 730 rC 64 435 :M f2_12 sf .436 .044(to be the set of input events and output events, respectively. Finally, we define)J 64 439 156 28 rC 64 467 :M f3_12 sf -.436( )A 220 467 :M psb currentpoint pse 64 439 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 4992 div 896 3 -1 roll exch div scale currentpoint translate 64 45 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (E) 6 371 sh (E) 589 371 sh (E) 1303 371 sh 224 ns (I) 555 201 sh (O) 1188 201 sh (i) 2933 467 sh (i) 1953 743 sh (m) 2408 743 sh (j) 4613 467 sh (j) 3664 743 sh (n) 4122 743 sh 384 /Symbol f1 (=) 264 371 sh (\310) 836 371 sh (=) 1644 371 sh /f3 {findfont 3 -1 roll .001 mul 3 -1 roll .001 mul matrix scale makefont dup /cf exch def sf} def 384 1000 1395 /Symbol f3 ({) 2515 404 sh (}) 3022 404 sh 384 /Symbol f1 (\310) 3263 371 sh 384 1000 1664 /Symbol f3 ({) 4185 429 sh (}) 4708 429 sh 224 /Symbol f1 (\316) 2033 743 sh (\316) 3750 743 sh /f2 {findfont matrix dup 2 .22 put makefont dup /cf exch def sf} def 384 /Symbol f2 (a) 2666 371 sh (b) 4361 371 sh 224 /Times-Roman f1 ([) 2159 743 sh (,) 2333 743 sh (]) 2586 743 sh ([) 3876 743 sh (,) 4050 743 sh (]) 4249 743 sh 224 /Times-Roman f1 (1) 2230 743 sh (1) 3947 743 sh 576 /MT-Extra f1 (U) 2112 458 sh (U) 3782 458 sh end MTsave restore pse gR gS 31 31 552 730 rC 220 452 :M f2_12 sf 4.633 .463( to be the complete set of terminal symbols)J 64 482 :M -.013(corresponding to events that are relevant to the abstraction being built.)A 64 512 :M -.337(Let)A 83 514 :M 3.666 .367( )J 91 502 9 12 rC 100 514 :M psb currentpoint pse 91 502 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 288 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (S) -3 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 100 512 :M f2_12 sf 3.03 .303( be the set of states that the module can be in. Then the module)J 64 530 :M -.024(specification for each state )A 215 520 26 12 rC 241 532 :M psb currentpoint pse 215 520 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 832 div 384 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh (S) 531 261 sh 384 /Symbol f1 (\316) 229 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 241 530 :M f2_12 sf -.015( has the following components:)A 64 561 :M (\245)S 82 546 82 15 rC 164 561 :M psb currentpoint pse 82 546 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 2624 div 480 3 -1 roll exch div scale currentpoint translate 64 59 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (prereq) 28 261 sh (E) 1644 261 sh (E) 2273 261 sh 224 ns (s) 1050 357 sh 384 /Symbol f1 (\315) 1262 261 sh (\264) 1967 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 164 556 :M f2_12 sf .939 .094( the modular prerequisite relation used to identify temporal)J 82 578 :M 2.871 .287(relationships between events in state )J 318 571 8 9 rC 326 580 :M psb currentpoint pse 318 571 :M psb /MTsave save def 30 dict begin currentpoint 3 -1 roll sub neg 3 1 roll sub 256 div 288 3 -1 roll exch div scale currentpoint translate 64 -37 translate /fs 0 def /cf 0 def /sf {exch dup /fs exch def dup neg matrix scale makefont setfont} def /f1 {findfont dup /cf exch def sf} def /ns {cf sf} def /sh {moveto show} def 384 /Times-Italic f1 (s) -6 261 sh end MTsave restore pse gR gS 31 31 552 730 rC 326 578 :M f2_12 sf 3.18 .318(. The prerequisite relation is)J 82 596 :M -.003(discussed further in Section\3123.2.2.)A -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 64 671.24 -.24 .24 207.24 671 .24 64 671 @a 64 684 :M f2_9 sf .385(40)A f2_10 sf 0 3 rm 1.45 .145(Because we are modelling externally visible behaviour, we do not allow blocks that have)J 0 -3 rm 64 699 :M -.013(neither \(externally visible\) inputs nor outputs.)A endp %%Page: 114 114 %%BeginPageSetup initializepage (nestor; page: 114 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 97 64 :M f1_10 sf -.018(Modular Specification)A 533 64 :M f0_12 sf -.781(33)A 97 100 :M f2_12 sf 2.819 .282(We will represent the behaviour of a module within a state with a )J 521 100 :M f1_12 sf -.248(state)A 97 118 :M .175(grammar)A f2_12 sf .486 .049(. This sentences in the language generated by this grammar are each)J 97 136 :M 1.046 .105(valid event sequences for the module while in that state. No interaction \(i.e.,)J 97 154 :M 1.581 .158(intermixing of events\) is permitted between the event sequences of different)J 97 172 :M .195 .019(states. A module must complete all of its transactions for one state before it can)J 97 190 :M -.014(proceed to another state.)A 99 205 445 218 rC 101 291 :M f0_12 sf -.688(Module)A 101 304 :M -.376(Inputs)A 494 294 :M -.688(Module)A 494 307 :M -.777(Outputs)A 146 384 -1 1 152 392 1 146 383 @a 151 393 -1 1 319 392 1 151 392 @a 319 393 -1 1 324 404 1 319 392 @a -1 -1 324 405 1 1 328 392 @b 328 393 -1 1 504 392 1 328 392 @a -1 -1 504 393 1 1 506 383 @b 305 419 :M -.688(Module)A 2 lw 259 209 387 381 7 @s 289 236 357 281 2 @s 289 311 357 356 2 @s 16 156 204 473 256 @k 358 257 -2 2 466 255 2 358 255 @a 299 261 :M -.984(Block 1)A 299 336 :M -.984(Block 2)A 356 317 133 34 rC 16 156 204 472 334 @k 357 335 -2 2 465 333 2 357 333 @a gR gS 172 239 133 34 rC 16 156 204 288 256 @k 173 257 -2 2 281 255 2 173 255 @a gR gS 150 289 20 55 rC -1 -1 152 296 1 1 158 290 @b 151 296 -1 1 160 300 1 151 295 @a 159 343 -1 1 167 343 1 159 342 @a gR gS 149 247 22 98 rC -1 -1 159 250 1 1 164 248 @b -1 -1 159 291 1 1 158 249 @b -1 -1 160 343 1 1 159 300 @b gR gS 172 315 133 34 rC 16 156 204 288 332 @k 173 333 -2 2 281 331 2 173 331 @a gR gS 99 205 445 218 rC 175 269 :M f0_12 sf -.675(Input Event )A 175 282 :M -.612(Stream 1 )A 176 313 :M -.675(Input Event )A 176 326 :M -.612(Stream 2 )A 390 272 :M -.851(Output Event )A 390 285 :M -.612(Stream 1 )A 391 312 :M -.851(Output Event )A 391 325 :M -.612(Stream 2 )A 472 248 -1 1 480 249 1 472 247 @a -1 -1 480 291 1 1 479 249 @b 479 291 -1 1 490 295 1 479 290 @a -1 -1 481 301 1 1 488 295 @b -1 -1 481 343 1 1 480 301 @b -1 -1 474 347 1 1 480 342 @b gR gS 31 31 552 730 rC 212 445 :M f2_12 sf -.023(Figure 3.1:)A 284 445 :M -.01(A Module with Two Blocks)A 97 475 :M 1.334 .133(In addition, a module may be composed of a number of causally independent)J 97 493 :M .037 .004(substructures referred to as )J 256 493 :M f1_12 sf -.199(blocks)A 290 493 :M f2_12 sf .082 .008( \(see Figure\3123.1\). A block can be thought of as)J 97 511 :M 2.879 .288(a sub-module that has been composed with another sub-module, with no)J 97 529 :M 1.79 .179(connections between them. Each block receives input events and generates)J 97 547 :M .207 .021(output events independently of other blocks within the module. The events that)J 97 565 :M 1.203 .12(make up a complete transaction are specific to each block. In this sense, the)J 97 583 :M -.007(activities of one block have no effect whatsoever on the activities of another block)A 97 601 :M 2.541 .254(within the module.)J f2_9 sf 0 -3 rm .461(39)A 0 3 rm f2_12 sf 1.544 .154( The definition of a block relates to the structure of a)J 97 619 :M .489 .049(module and is therefore constant across the various states that a module might)J 97 637 :M .403 .04(be in. However, the events that make up a complete transaction for a block are)J 97 655 :M -.018(particular to each state that the module is in.)A -4096 -4095 -1 1 -4094 -4095 1 -4096 -4096 @a 97 683.24 -.24 .24 240.24 683 .24 97 683 @a 97 696 :M f2_9 sf (39)S f2_10 sf 0 3 rm -.005(Section\3123.4.9 gives an example of the specification of a two block specification.)A 0 -3 rm endp %%Page: 115 115 %%BeginPageSetup initializepage (nestor; page: 115 of 162)setjob %%EndPageSetup -31 -31 :T gS 31 31 552 730 rC 64 64 :M f0_12 sf -.781(32)A 262 64 :M f1_10 sf -.01(The Composition of Property-Preserving Event Systems)A 64 102 :M f0_14 sf -.484(3.2)A 109 102 :M (M)S 123 102 :M f0_12 sf -.164(ODULAR )A 184 102 :M f0_14 sf -.122(R)A f0_12 sf -.104(EPRESENTATION)A 64 133 :M f2_12 sf 3.075 .307(This section will introduce a specification for a module based on formal)J 64 151 :M .004 0(grammars. We will begin by informally describing some basic notions relating to)J 64 169 :M -.02(the structure and operation of a module.)A 64 199 :M 3.497 .35(A module operates by accepting one or more )J 355 199 :M f1_12 sf 3.32 .332(input events)J f2_12 sf 2.501 .25(, and possibly)J 64 217 :M .175 .017(responding by generating one or more )J 280 217 :M f1_12 sf .138 .014(output events)J f2_12 sf .101 .01(. Conceptually, input events)J 64 235 :M 1.89 .189(to a module originate in the environment or from another module. Output)J 64 253 :M .447 .045(events are generated by the module and sent somewhere else \(either to another)J 64 271 :M 1.187 .119(module or to the external environment\). Each stream of input events will be)J 64 289 :M .314 .031(called a )J f1_12 sf .668 .067(module input)J f2_12 sf .347 .035(, and each stream of output events will be called a )J 473 289 :M f1_12 sf -.13(module)A 64 307 :M -.2(output)A 100 307 :M f2_12 sf .885 .089(. In modelling a particular system, the module inputs and outputs may)J 64 325 :M .162 .016(not necessarily correspond to physical channels. The occurrence of certain input)J 64 343 :M .167 .017(or output events might denote the completion of abstractly-defined operations or)J 64 361 :M -.083(requirements.)A 64 391 :M 3.318 .332(Later in this section, we will develop the notion of a )J 409 391 :M f1_12 sf 1.796 .18(module grammar)J f2_12 sf (.)S 64 409 :M 1.323 .132(Sentences in the language generated from the module grammar will be valid)J 64 427 :M .534 .053(event sequences formed from a properly ordered succession of input and output)J 64 445 :M -.028(events for the specified module.)A 64 475 :M .745 .075(We will use the term )J f1_12 sf 1.753 .175(complete transaction)J 308 475 :M f2_12 sf 1.258 .126( to describe a complete set of input)J 64 493 :M 1.58 .158(events and the corresponding, causally related output events at a particular)J 64 511 :M .582 .058(module. A )J 130 511 :M f1_12 sf 1.069 .107(partial transaction)J f2_12 sf .537 .054( is one in which output events are pending, or in)J 64 529 :M .81 .081(which only a partial set of inputs has been provided to a module. Our module)J 64 547 :M .252 .025(grammars will generate sentences \(i.e., valid event sequences\) that are made up)J 64 565 :M -.017(of zero or more complete transactions.)A 64 595 :M 1.746 .175(It is assumed that the represented module is able to move through a set of)J 64 613 :M