From adrian.lawrence@computing-services.oxford.ac.uk Sun Oct 31 15:49:07 2004 From: Adrian Lawrence To: occam-com@ukc.ac.uk Date: Tue, 2 Mar 1999 00:21:57 +0000 (GMT) Subject: 28K of postscript: Conflicting Priorities in occam Content-Transfer-Encoding: 8bit Content-Type: text/plain; charset=ISO-8859-1 MIME-Version: 1.0 X-Mailer: ELM [version 2.4 PL24 PGP2] Message-ID: I promised to post Example 8.14 in its original form here. ================== cut here for postscript ========================== %!PS-Adobe-2.0 %%Creator: dvips(k) 5.78 Copyright 1998 Radical Eye Software (www.radicaleye.com) %%Title: cspp.dvi %%Pages: 2 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%DocumentFonts: Times-Roman Times-Italic Times-Bold Courier Helvetica %%EndComments %DVIPSCommandLine: dvips -p50 -l51 cspp %DVIPSParameters: dpi=360, compressed %DVIPSSource: TeX output 1999.03.01:1212 %%BeginProcSet: texc.pro %! /TeXDict 300 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if} forall round exch round exch]setmatrix}N /@landscape{/isls true N}B /@manualfeed{statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{ /nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{ /sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0] N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{ 128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 sub]/id ch-image N /rw ch-width 7 add 8 idiv string N /rc 0 N /gp 0 N /cp 0 N{rc 0 ne{rc 1 sub /rc X rw}{G}ifelse}imagemask restore}B /G{{id gp get /gp gp 1 add N dup 18 mod S 18 idiv pl S get exec}loop}B /adv{cp add /cp X}B /chg{rw cp id gp 4 index getinterval putinterval dup gp add /gp X adv}B /nd{/cp 0 N rw exit}B /lsh{rw cp 2 copy get dup 0 eq{pop 1}{ dup 255 eq{pop 254}{dup dup add 255 and S 1 and or}ifelse}ifelse put 1 adv}B /rsh{rw cp 2 copy get dup 0 eq{pop 128}{dup 255 eq{pop 127}{dup 2 idiv S 128 and or}ifelse}ifelse put 1 adv}B /clr{rw cp 2 index string putinterval adv}B /set{rw cp fillstr 0 4 index getinterval putinterval adv}B /fillstr 18 string 0 1 17{2 copy 255 put pop}for N /pl[{adv 1 chg} {adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{ adv rsh nd}{1 add adv}{/rc X nd}{1 add set}{1 add clr}{adv 2 chg}{adv 2 chg nd}{pop nd}]dup{bind pop}forall N /D{/cc X dup type /stringtype ne{] }if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{ cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore userdict /eop-hook known{eop-hook}if showpage}N /@start{userdict /start-hook known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 2 string 0 1 255{IE S dup 360 add 36 4 index cvrs cvn put}for pop 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V{}B /RV statusdict begin /product where{pop false[ (Display)(NeXT)(LaserWriter 16/600)]{dup length product length le{dup length product exch 0 exch getinterval eq{pop true exit}if}{pop}ifelse} forall}{false}ifelse end{{gsave TR -.1 .1 TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1 .1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave newpath transform round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail {dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}B /c{-4 M} B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{3 M}B /k{ 4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w}B /q{ p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{3 2 roll p a}B /bos{/SS save N}B /eos{SS restore}B end %%EndProcSet %%BeginProcSet: 8r.enc % @@psencodingfile@{ % author = "S. Rahtz, P. MacKay, Alan Jeffrey, B. Horn, K. Berry", % version = "0.6", % date = "22 June 1996", % filename = "8r.enc", % email = "kb@@mail.tug.org", % address = "135 Center Hill Rd. // Plymouth, MA 02360", % codetable = "ISO/ASCII", % checksum = "119 662 4424", % docstring = "Encoding for TrueType or Type 1 fonts to be used with TeX." % @} % % Idea is to have all the characters normally included in Type 1 fonts % available for typesetting. This is effectively the characters in Adobe % Standard Encoding + ISO Latin 1 + extra characters from Lucida. % % Character code assignments were made as follows: % % (1) the Windows ANSI characters are almost all in their Windows ANSI % positions, because some Windows users cannot easily reencode the % fonts, and it makes no difference on other systems. The only Windows % ANSI characters not available are those that make no sense for % typesetting -- rubout (127 decimal), nobreakspace (160), softhyphen % (173). quotesingle and grave are moved just because it's such an % irritation not having them in TeX positions. % % (2) Remaining characters are assigned arbitrarily to the lower part % of the range, avoiding 0, 10 and 13 in case we meet dumb software. % % (3) Y&Y Lucida Bright includes some extra text characters; in the % hopes that other PostScript fonts, perhaps created for public % consumption, will include them, they are included starting at 0x12. % % (4) Remaining positions left undefined are for use in (hopefully) % upward-compatible revisions, if someday more characters are generally % available. % % (5) hyphen appears twice for compatibility with both ASCII and Windows. % /TeXBase1Encoding [ % 0x00 (encoded characters from Adobe Standard not in Windows 3.1) /.notdef /dotaccent /fi /fl /fraction /hungarumlaut /Lslash /lslash /ogonek /ring /.notdef /breve /minus /.notdef % These are the only two remaining unencoded characters, so may as % well include them. /Zcaron /zcaron % 0x10 /caron /dotlessi % (unusual TeX characters available in, e.g., Lucida Bright) /dotlessj /ff /ffi /ffl /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef % very contentious; it's so painful not having quoteleft and quoteright % at 96 and 145 that we move the things normally found there down to here. /grave /quotesingle % 0x20 (ASCII begins) /space /exclam /quotedbl /numbersign /dollar /percent /ampersand /quoteright /parenleft /parenright /asterisk /plus /comma /hyphen /period /slash % 0x30 /zero /one /two /three /four /five /six /seven /eight /nine /colon /semicolon /less /equal /greater /question % 0x40 /at /A /B /C /D /E /F /G /H /I /J /K /L /M /N /O % 0x50 /P /Q /R /S /T /U /V /W /X /Y /Z /bracketleft /backslash /bracketright /asciicircum /underscore % 0x60 /quoteleft /a /b /c /d /e /f /g /h /i /j /k /l /m /n /o % 0x70 /p /q /r /s /t /u /v /w /x /y /z /braceleft /bar /braceright /asciitilde /.notdef % rubout; ASCII ends % 0x80 /.notdef /.notdef /quotesinglbase /florin /quotedblbase /ellipsis /dagger /daggerdbl /circumflex /perthousand /Scaron /guilsinglleft /OE /.notdef /.notdef /.notdef % 0x90 /.notdef /.notdef /.notdef /quotedblleft /quotedblright /bullet /endash /emdash /tilde /trademark /scaron /guilsinglright /oe /.notdef /.notdef /Ydieresis % 0xA0 /.notdef % nobreakspace /exclamdown /cent /sterling /currency /yen /brokenbar /section /dieresis /copyright /ordfeminine /guillemotleft /logicalnot /hyphen % Y&Y (also at 45); Windows' softhyphen /registered /macron % 0xD0 /degree /plusminus /twosuperior /threesuperior /acute /mu /paragraph /periodcentered /cedilla /onesuperior /ordmasculine /guillemotright /onequarter /onehalf /threequarters /questiondown % 0xC0 /Agrave /Aacute /Acircumflex /Atilde /Adieresis /Aring /AE /Ccedilla /Egrave /Eacute /Ecircumflex /Edieresis /Igrave /Iacute /Icircumflex /Idieresis % 0xD0 /Eth /Ntilde /Ograve /Oacute /Ocircumflex /Otilde /Odieresis /multiply /Oslash /Ugrave /Uacute /Ucircumflex /Udieresis /Yacute /Thorn /germandbls % 0xE0 /agrave /aacute /acircumflex /atilde /adieresis /aring /ae /ccedilla /egrave /eacute /ecircumflex /edieresis /igrave /iacute /icircumflex /idieresis % 0xF0 /eth /ntilde /ograve /oacute /ocircumflex /otilde /odieresis /divide /oslash /ugrave /uacute /ucircumflex /udieresis /yacute /thorn /ydieresis ] def %%EndProcSet %%BeginProcSet: texps.pro %! TeXDict begin /rf{findfont dup length 1 add dict begin{1 index /FID ne 2 index /UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics exch def dict begin Encoding{exch dup type /integertype ne{pop pop 1 sub dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def} ifelse}forall Metrics /Metrics currentdict end def[2 index currentdict end definefont 3 -1 roll makefont /setfont cvx]cvx def}def /ObliqueSlant {dup sin S cos div neg}B /SlantFont{4 index mul add}def /ExtendFont{3 -1 roll mul exch}def /ReEncodeFont{/Encoding exch def}def end %%EndProcSet TeXDict begin 39158280 55380996 1000 360 360 (cspp.dvi) @start /Fa 137[30 12[13 4[33 100[{TeXBase1Encoding ReEncodeFont}3 59.7758 /Helvetica rf /Fb 134[36 36 9[36 11[36 36 12[36 36 36 1[36 36 36 1[36 2[36 36 1[36 2[36 1[36 1[36 4[36 8[36 15[36 33[{TeXBase1Encoding ReEncodeFont}21 59.7758 /Courier rf /Fc 150[11 105[{TeXBase1Encoding ReEncodeFont}1 39.8506 /Times-Italic rf /Fd 135[30 7[33 30 1[50 17 6[27 1[27 1[30 20[40 6[40 12[30 30 30 30 30 30 30 30 2[15 46[{TeXBase1Encoding ReEncodeFont}19 59.7758 /Times-Bold rf /Fe 134[27 1[40 27 30 17 23 23 30 30 30 30 1[17 27 17 17 30 1[17 27 30 27 30 30 8[37 3[33 30 1[43 37 3[33 2[20 7[37 18[15 1[15 44[{TeXBase1Encoding ReEncodeFont}32 59.7758 /Times-Italic rf /Ff 107[27 27 24[27 30 30 43 30 30 17 23 20 30 30 30 30 47 17 30 1[17 30 30 20 27 30 27 30 27 3[20 1[20 6[37 33 2[33 6[20 43 2[37 1[40 40 43 6[17 1[30 30 1[30 30 30 30 30 30 1[15 20 15 2[20 20 37[33 2[{TeXBase1Encoding ReEncodeFont}53 59.7758 /Times-Roman rf %DVIPSBitmapFont: Fg cmsy10 17.28 1 /Fg 1 118 df<007FB712F8B812FCA300F0C9123CB3B3AA006016182E337BB239>117 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fh cmr8 8 4 /Fh 4 52 df<1306ADB612F0A2D80006C7FCAD1C1C7E9721>43 D<12035A123F12C71207 B3A3EAFFF80D1A7C9915>49 DII E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fi msbm10 12 1 /Fi 1 82 df81 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fj cmex10 12 10 /Fj 10 62 df<13021304130813101330136013C0A2EA0180120313005AA2120EA2121E 121CA2123C1238A31278A4127012F0B012701278A41238A3123C121CA2121E120EA27EA2 7E13801201EA00C0A21360133013101308130413020F4677811B>0 D<7E12407E7E12187E7EA27E1380120113C0A2EA00E0A213F01370A213781338A3133CA4 131C131EB0131C133CA41338A313781370A213F013E0A2EA01C0A21380120313001206A2 5A5A12105A5A5A0F467E811B>I<1460EB0380EB0E00133C5B5BA2485AB3A4485A5B48C7 FC121E123812E0A21238121E12076C7E7F6C7EB3A46C7EA213787F130EEB0380EB006013 46788123>8 D<12C01238120E6C7E6C7E6C7EA26C7EB3A4137813387F130FEB0380EB00 F0A2EB0380EB0F00131C5B13785BB3A4485AA2485A485A000EC7FC123812C01446798123 >I<1470EB01F01307EB0FE0EB1F80EB3F00137E13FE485A485A485AA2485A121F5B123F A25B127FA390C7FC5AB3AE14366A7E35>56 D<12E012F812FE127FEA1F806C7E6C7E7F6C 7E6C7E6C7EA2137F1480133F14C0A2131F14E0A3130F14F0B3AE1436767E35>IIIII E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fk stmary10 12 1 /Fk 1 36 df35 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fl cmmi12 12 3 /Fl 3 62 df<127812FCA4127806067B8510>58 D<127812FCA212FEA2127A1202A41204 A31208A212101220124007127B8510>I<140C141CA21438A31470A314E0A3EB01C0A3EB 0380A3EB0700A3130EA35BA35BA35BA35BA3485AA3485AA348C7FCA3120EA35AA35AA35A A35AA25A163C7DAC1D>61 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fm msam10 12 5 /Fm 5 75 df3 D<80497EA2497E497EA2497E497EA2497EA2497E90B57EA24880A248804880A248804880 A24880A24880B71280A26C1500A26C5C6C5CA26C5CA26C5C6C5CA26C5CA26C5C6D90C7FC A26D5A6D5AA26D5AA26D5A6D5AA26D5AA221347DAB28>7 D<12C07EA31270A37E123C7E 7E6C7EEA03E0EA01F8EA007EEB3FE0903807FF800101EBFFE0EB001F49B5FC0107EB8000 D93FE0C7FC017EC8FCEA01F8EA03E0EA078048C7EA1FE0001EEB01FF48130F003890383F E0004801FEC7FCEB03F0EB07C04848C8FC131E5B485AEA00705BA2485AA4485A1201232E 7BA42E>60 D<126012F012FCB4FC13C013F013FC13FF14C014F014FC14FF8115E015F815 FEEDFF8016E0A31680EDFE0015F815E0158092C7FC14FC14F014C091C8FC13FC13F013C0 90C9FC12FC12F05A23257B9F2E>73 D<16C01503150F153F15FF1403140F5C147F49B5FC 1307131F137F48B6FC5A120F123FB7FCA3123F120F12037E6C7E131F130713016D7E141F 8014031400153F150F1503150122257A9F2E>I E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fn lasy10 12 1 /Fn 1 51 df<007FB61280B7FCA200E0C71203B3A9B7FCA27E21217BA42D>50 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fo cmr12 12 7 /Fo 7 64 df6 D<130813101320134013C0EA0180A2EA03001206A2120E120C121CA212181238A212 301270A512F05AAD7E1270A512301238A21218121CA2120C120E1206A27EEA0180A2EA00 C013401320131013080D3D7AAC17>40 D<7E12407E7E12187EA27E7EA21380120113C0A2 120013E0A213601370A513781338AD13781370A5136013E0A213C01201A2138012031300 A212065AA25A12105A5A5A0D3D7DAC17>I<137E3801C380380700E0000E1370001E1378 001C1338003C133CA20038131C0078131EA400F8131FAF0078131EA4007C133E003C133C A2001C1338001E1378000E13706C13E03801C38038007E0018297EA71D>48 D<132013E01201120F12FF12F11201B3AD487EB512C0A212287BA71D>I61 D63 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fp cmsy10 12 20 /Fp 20 120 df0 D<0107B512E0131F137FD801F8C8FCEA03E0 EA078048C9FC121E121C5AA25AA35AA91270A37EA27E121E7E6C7EEA03E0EA01FCD8007F B512E0131F130390C9FCA9003FB612E05A7E23317BA52E>18 D<130EA35BA2133C133813 7813705B1201485A485A001FCBFC48B812F0B912F8003F17F06CCBFCEA07806C7E6C7E12 00137013781338133C131CA27FA3351F7D9D3C>32 DI<903803FFF8131F137FD801FCC7FCEA03E0EA078048C8FC12 1E121C5AA25AA35AA3B612F8A300E0C8FCA31270A37EA27E121E7E6C7EEA03E0EA01FC39 007FFFF8131F13031D257BA028>50 D<12E0AA12F012F812F012E0AA05177D9900>55 D<14301470A2EB7CE0EA0183EA0701EA0E00EA0C01001C13F0003813F8EB03B8A2007813 BC3870071CA300F0131E130EA3131CA31338A41370A313E0A3EAF1C00071131CA3387B80 3C003B1338A2EA3F006C1370A2000E13E0380F01C0EB8300EA0E7C48C7FCA2121817327D AD1E>59 D<1618167816F8A31501A21503A21506A2150CA21518153815301570156015E0 15C0EC018014034B7E5C140E167C5C5CA25C9138E7FFFC91B5FC5B90390380007C167E49 C7FC130ED8601E143EEA703CD87878143FD8FFF815084915F06C48EC1FC06C4815006C48 91C7FC6CCAFC2D2E7EAA30>65 D<0102EB1F80010EEBFFE0D93E0313F09039FE0E0FF839 033C18030000EB3001EC6000EB7CC0D97D8013F0137F91C712E0ED01C0017E1480ED0300 4913061518491360EC0380EC1FF83901F03FFE91B5FC0200138049EB3FC0151F0003EC0F E0491307A2150312075BA216C048C7FC1680ED0700001E140601205BD81CF05BD83DF85B 393BFF01C0007901FFC7FC006013FC38C01FE0252B7EA927>I<0060EC018000E01403B3 A80070EC0700A26C140E003C141E6C5C6C6C13F83907F007F00001B512C06C6C90C7FCEB 0FF821257DA328>91 DI<14F8EB03C0EB0F00131E5B 5BB3A25BA2485AEA078000FEC7FCA2EA0780EA01E06C7EA21378B3A27F7F7FEB03C0EB00 F8153C7CAC1E>102 D<12F8120FEA03C06C7E6C7E1378B3A27FA27F1307EB01F8A2EB07 00131E5BA25BB3A25B485A485A000FC7FC12F8153C7CAC1E>I<130C131CA21338A21370 A313E0A3EA01C0A2EA0380A3EA0700A3120EA25AA35AA35AA25AA31270A27EA37EA37EA2 7EA3EA0380A3EA01C0A2EA00E0A31370A31338A2131CA2130C0E3D7BAC17>I<12C07EA2 1270A27EA37EA37EA27EA3EA0380A3EA01C0A2EA00E0A31370A31338A2131CA31338A213 70A313E0A3EA01C0A2EA0380A3EA0700A3120EA25AA35AA35AA25AA25A0E3D7DAC17>I< 12E0B3B3B3A6033C79AC11>II<12C07EA2 1270A37EA37EA27EA37EA36C7EA36C7EA36C7EA31370A37FA27FA37FA37FA3EB0380A3EB 01C0A3EB00E0A31470A21438A3141CA3140EA21406173C7DAC1E>110 D117 D<007FB612F8B7FC7EC91238 B3AD007FB612F8B7FC7ECAFCA9007FB612F016F8A225317DA52E>119 D E %EndDVIPSBitmapFont end %%EndProlog %%BeginSetup %%Feature: *Resolution 360dpi TeXDict begin %%PaperSize: A4 %%EndSetup %%Page: 50 1 50 0 bop 0 251 a Ff(so)17 b(we)f(might)g(e)o(xpect)f(that)g Fe(P)628 206 y Fp( )-40 b(\000)638 251 y Fm(\003)10 b Fe(Q)15 b Fp(w)g Fe(P)k Fn(2)h Fe(Q)p Ff(.)k(Ho)o(we)o(v)o(er)15 b(if)h(we)h(consider)e(circuits)g(implementi)o(ng)f Fe(P)2186 206 y Fp( )-40 b(\000)2195 251 y Fm(\003)11 b Fe(Q)0 323 y Ff(and)19 b Fe(P)25 b Fn(2)g Fe(Q)20 b Ff(and)f(signalling)e (their)i(readiness)f(to)h(perform)f Fe(P)h Ff(and)g Fe(Q)h Ff(on)g(separate)d(wires,)j(then)f Fe(P)25 b Fn(2)g Fe(Q)0 408 y(always)20 b Ff(has)h(a)g(property)f(which)g Fe(P)764 363 y Fp( )-40 b(\000)774 408 y Fm(\003)10 b Fe(Q)22 b Ff(ne)o(v)o(er)e(possesses.)37 b(In)21 b(particular)n(,)f(it)h(can)f (of)o(fer)g(both)g Fe(P)h Ff(and)g Fe(Q)0 502 y Ff(simultaneously)13 b(while)h Fe(P)563 457 y Fp( )-40 b(\000)573 502 y Fm(\003)10 b Fe(Q)16 b Ff(can)f(ne)o(v)o(er)f(do)h(so.)21 b(In)16 b(conte)o(xts)e(where)g(this)i(is)f(not)g(signi\002cant,)32 b Fm(<)i Ff(is)16 b(the)0 574 y(rele)o(v)o(ant)11 b(relation.)16 b Fd(occam)e Ff(pro)o(vides)g(such)g(a)g(conte)o(xt:)i(it)e(only)h (permits)e(constrained)f(sorts)j(of)f(interaction)0 646 y(between)h(prioritized)e(processes.)22 b(In)16 b(the)f(class)h(of)g (CSPP)h(processes)e(implementing)e(occam,)i(no)h(process)0 731 y(can)e(tell)f Fe(P)j Fn(2)h Fe(Q)e Ff(from)f Fe(P)530 686 y Fp( )-40 b(\000)539 731 y Fm(\003)11 b Fe(Q)p Ff(.)p 732 731 30 30 v 108 w([8.11])0 936 y Fd(Lemma)j(8.1)29 b Fe(If)14 b(P)i Fo(=)h Fe(P)519 945 y Fh(1)558 936 y Fp(u)g Fe(P)652 945 y Fh(2)690 936 y Fe(then)d(tr)o(aces)9 b(P)16 b Fo(=)g Fe(tr)o(aces)9 b(P)1270 945 y Fh(1)1307 936 y Fp([)k Fe(tr)o(aces)c(P)1552 945 y Fh(2)0 1067 y Ff(This)14 b(is,)h(of)g(course,)f(blindingly)e(ob)o(vious)j(from)f (equation)f(\(32\))h(on)h(page)f(24.)78 b Fm(\007)p Ff([8.1])0 1271 y Fd(Example)14 b(8.12)29 b Fe(The)16 b(sequence)g(P)755 1280 y Fh(1)778 1271 y Fl(;)10 b Fe(P)841 1280 y Fh(2)864 1271 y Fl(;)g Fe(P)927 1280 y Fh(3)951 1271 y Fl(;)g(:)g(:)g(:)28 b Fe(with)16 b(P)1230 1280 y Fc(i)1264 1271 y Fo(=)1330 1278 y Fg(u)1387 1271 y Fp(f)p Fe(q)21 b Fp(!)f Fe(Stop)g Fp(j)h Fe(q)f Fp(2)h Fo(\(0)p Fl(;)10 b Fo(1)p Fl(=)p Fe(i)p Fo(\))p Fp(g)17 b Fe(wher)n(e)f(q)h(is)0 1344 y(r)o(ational)d(or)h(r)n(eal)f(is)h(a)f(dir)n(ected)f(set)h(with)g(no)h (join.)0 1474 y Ff(This)c(is)g(another)f(e)o(xample)f(of)i(unbounded)f (nondeterminism)o(:)k(it)c(is)i(not)e(really)g(dif)o(ferent)f(from)h(e) o(xample)f(7.1)0 1547 y(on)14 b(page)f(33)h(in)g(principle.)h(But)f(it) f(is)h(more)g(natural,)e(although)g(more)h(restricted.)j(Here)d Fe(P)1899 1556 y Fc(i)p Fh(+1)1977 1547 y Fp(w)e Fe(P)2071 1556 y Fc(i)2098 1547 y Ff(and)j(also)0 1619 y Fe(P)37 1628 y Fc(i)p Fh(+1)123 1619 y Fm(<)19 b Fe(P)225 1628 y Fc(i)254 1619 y Ff(so)d Fp(f)p Fe(P)390 1628 y Fc(i)403 1619 y Fp(g)f Ff(is)h(a)g(directed)d(set)j(under)f(both)g Fp(w)h Ff(and)f Fm(<)p Ff(.)22 b(The)15 b(only)h(candidate)d(for)i(an)h (upper)f(bound)0 1691 y(is)j Fe(Stop)o Ff(,)g(b)o(ut)f(it)g(cannot)g (be)g(compared)e(with)i(the)g Fe(P)1098 1700 y Fc(i)1129 1691 y Ff(under)g(either)f(the)h(order)g(or)g(the)g(pre-order)m(.)25 b(Here)17 b(we)0 1763 y(require)c Fi(Q)20 b Fp(\022)d Fo(\006)p Ff(,)f(at)e(least.)p 643 1763 V 106 w([8.12])0 1968 y Fd(Example)g(8.13)29 b Fo(\()p Fe(a)16 b Fp(!)g Fe(Stop)g Fn(2)g Fe(b)h Fp(!)f Fe(Stop)p Fo(\))g Fp(n)g(f)p Fe(b)p Fp(g)33 b Fo(=)g(\()p Fe(a)16 b Fp(!)h Fe(Stop)o Fo(\))f Fp(u)h Fe(Stop)0 2099 y Ff(Applying)d(equation)f(\(55\))h(on)h (page)f(31)g(to)h Fo(\()p Fe(a)h Fp(!)g Fe(Stop)g Fn(2)h Fe(b)f Fp(!)g Fe(Stop)p Fo(\))g Fp(n)h(f)p Fe(b)p Fp(g)p Ff(,)d(we)h(\002nd)g(tw)o(o)g(beha)o(viours:)146 2195 y Fj(8)146 2249 y(<)146 2356 y(:)239 2262 y Fp(hi)i(7!)p Fe(X)i Fp(7!)d(f)p Fe(a)p Fp(g)d(\\)g Fe(X)s Fl(;)209 2387 y Fp(h)p Fe(a)p Fp(i)k(7!)p Fe(X)i Fp(7!)d(;)716 2195 y Fj(9)716 2249 y(=)716 2356 y(;)898 2318 y Fp(fhi)h(7!)g Fe(X)i Fp(7!)d(;g)p 60 2530 V 90 2530 a Ff([8.13])0 2735 y Fd(Example)e(8.14)29 b Fo(\()p Fe(a)16 b Fp(!)g Fe(Stop)627 2690 y Fp( )-40 b(\000)637 2735 y Fm(\003)10 b Fe(b)16 b Fp(!)h Fe(Stop)o Fo(\))f Fp(n)h(f)p Fe(b)p Fp(g)f Fo(=)g Fe(a)h Fp(!)f Fe(Stop)0 2866 y Ff(Equation)d(\(55\))h(gi)o(v)o(es)146 3003 y Fp(fhi)j(7!)g Fe(X)h Fp(7!)f(f)p Fe(a)p Fp(g)c(\\)g Fe(X)s Fl(;)26 b Fp(h)p Fe(a)p Fp(i)17 b(7!)f Fe(X)j Fp(7!)d(;g)0 3140 y Ff(in)e(an)h(ob)o(vious)f(notation.)j(The)c(other)h (hidden)g(beha)o(viour)f(ho)o(we)o(v)o(er)g(yields)g(only)i(the)f (partial:)146 3278 y Fp(fhi)j(7!)g Fe(X)h Fp(7!)f(f)p Fe(a)p Fp(g)c(\\)g Fe(X)s Fp(g)1118 3427 y Ff(50)p eop %%Page: 51 2 51 1 bop 0 244 a Ff(which)16 b(matches)f(the)h(stem)g(of)h(the)f(last)h (case.)23 b(Since)16 b(equation)f(\(55\))i(requires)f(that)p 1802 197 37 3 v 15 w Fe(A)21 b Fp(2)f(A)-6 b(B)r Ff(,)18 b(that)d(partial)0 316 y(beha)o(viour)e(is)i(eliminate)o(d)d(and)i(we)h (ha)o(v)o(e)146 465 y Fp(B)197 417 y Fj(\000)225 465 y Fo(\()p Fe(a)h Fp(!)g Fe(Stop)477 420 y Fp( )-40 b(\000)487 465 y Fm(\003)10 b Fe(b)17 b Fp(!)f Fe(Stop)o Fo(\))h Fp(n)f(f)p Fe(b)p Fp(g)948 417 y Fj(\001)992 465 y Fo(=)1054 417 y Fj(\010)1089 465 y Fp(fhi)h(7!)f Fe(X)j Fp(7!)d(f)p Fe(a)p Fp(g)d(\\)g Fe(X)s Fl(;)26 b Fp(h)p Fe(a)p Fp(i)17 b(7!)g Fe(X)h Fp(7!)f(;g)1990 417 y Fj(\011)88 597 y Ff(This)e(e)o(xample)e(demonstrates)g(some)i(of)h(the)f(limitatio)o(ns) e(of)j(the)f(untimed)e(theory)l(.)20 b(At)c(\002rst)g(sight,)f(one)0 682 y(w)o(ould)g(e)o(xpect)e(that)g Fo(\()p Fe(a)k Fp(!)f Fe(Stop)690 637 y Fp( )-40 b(\000)700 682 y Fm(\003)11 b Fe(b)16 b Fp(!)h Fe(Stop)o Fo(\))f Fp(n)h(f)p Fe(b)p Fp(g)d Ff(w)o(as)i(a)e(model)g(for)0 805 y Fb(CHAN)35 b(OF)h(INT)f(b:)0 877 y(PAR)72 949 y(b)g(!)h(1)72 1022 y(PRI)f(ALT)143 1094 y(a)h(?)g(x)215 1166 y(STOP)143 1238 y(b)g(?)g(any)215 1311 y(STOP)0 1433 y Ff(Ho)o(we)o(v)o(er)n(,)12 b(the)g(occam)g(process)h(is)g(not)g(equi)o(v)o(alent)d(to)j Fe(in)p Fo(?)p Fe(a)j Fp(!)g Fe(Stop)d Ff(for)g(it)g(will)g(not)g (\223block\224)e(on)j(the)e(input.)0 1505 y(The)h(discrepanc)o(y)f (arises)i(because)e(the)h(untimed)g(theory)g(does)g(not)h(model)f(an)h (en)n(vironment)d(that)i(can)g(alter)0 1578 y(its)h(of)o(fer)g(between) f(e)o(v)o(ents.)p 659 1578 30 30 v 107 w([8.14])0 1772 y Fd(Example)h(8.15)29 b Fo(\()p Fe(a)16 b Fp(!)g Fe(Stop)627 1727 y Fp(\000)-40 b(!)637 1772 y Fm(\003)10 b Fe(b)16 b Fp(!)h Fe(Stop)o Fo(\))f Fp(n)h(f)p Fe(b)p Fp(g)f Fo(=)g Fe(Stop)0 1895 y Ff(Beha)o(viour)146 1979 y Fj(\010)181 2028 y Fp(hi)h(7!)g Fe(X)h Fp(7!)f(f)p Fe(b)p Fp(g)f Fm(J)h Fe(b)g Fp(2)f Fe(X)j Fm(I)e Fe(X)e Fp(\\)f(f)p Fe(a)p Fp(g)p Fl(;)c Fp(h)p Fe(a)p Fp(i)16 b(7!)h Fe(X)i Fp(7!)d(;)1397 1979 y Fj(\011)0 2160 y Ff(gi)o(v)o(es)146 2292 y Fp(hi)h(7!)g Fe(X)i Fp(7!)d(;)0 2431 y Ff(and)21 b(the)f(trailing)f Fp(h)p Fe(a)p Fp(i)29 b(7!)f Fe(X)j Fp(7!)d(;)21 b Ff(is)g(pruned)f(by)i(the)e(requirement)p 1530 2384 37 3 v 18 w Fe(A)28 b Fp(2)g(A)-6 b(B)r Ff(.)38 b(The)20 b(other)g(beha)o(viour)0 2503 y(produces)14 b(the)g(same)g(result.)p 683 2503 30 30 v 106 w([8.15])0 2698 y Fd(Example)g(8.16)29 b Fe(Let)146 2847 y(P)183 2856 y Fh(1)223 2847 y Fo(=)285 2798 y Fj(\000)313 2847 y Fo(\()p Fe(a)16 b Fp(!)g Fe(Stop)p Fo(\))g Fn(2)g Fo(\()p Fe(h)718 2856 y Fh(1)758 2847 y Fp(!)g Fe(Stop)p Fo(\))964 2798 y Fj(\001)1004 2847 y Fa(div)e Fp(ff)p Fe(a)p Fl(;)c Fe(h)1240 2856 y Fh(1)1263 2847 y Fp(gg)1323 2802 y( )-40 b(\000)1333 2847 y Fm(\003)1390 2798 y Fj(\000)1417 2847 y Fe(h)1447 2856 y Fh(2)1487 2847 y Fp(!)16 b Fe(Stop)1670 2798 y Fj(\001)146 2935 y Fe(P)183 2944 y Fh(2)223 2935 y Fo(=)285 2887 y Fj(\000)313 2935 y Fo(\()p Fe(a)g Fp(!)g Fe(Stop)p Fo(\))g Fn(2)g Fo(\()p Fe(h)718 2944 y Fh(1)758 2935 y Fp(!)g Fe(Stop)p Fo(\))964 2887 y Fj(\001)991 2890 y Fp( )-40 b(\000)1001 2935 y Fm(\003)1057 2887 y Fj(\000)1085 2935 y Fe(h)1115 2944 y Fh(2)1155 2935 y Fp(!)16 b Fe(Stop)1338 2887 y Fj(\001)0 3068 y Fe(Then)g Fo(\()p Fe(P)196 3077 y Fh(1)237 3068 y Fp(k)j Fe(P)323 3077 y Fh(2)346 3068 y Fo(\))f Fp(n)h(f)p Fe(h)496 3077 y Fh(1)519 3068 y Fl(;)10 b Fe(h)575 3077 y Fh(2)599 3068 y Fp(g)16 b Fe(liveloc)o(ks)d(on)j(the)f(of)o(fer)g Fp(f)p Fe(a)p Fp(g)p Fe(,)h(b)o(ut)f Fo(\()p Fe(P)1434 3077 y Fh(1)1476 3068 y Fp(n)j(f)p Fe(h)1584 3077 y Fh(1)1608 3068 y Fl(;)10 b Fe(h)1664 3077 y Fh(2)1688 3068 y Fp(g)p Fo(\))18 b Fp(k)g Fo(\()p Fe(P)1867 3077 y Fh(2)1907 3068 y Fp(n)f(f)p Fe(h)2014 3077 y Fh(1)2037 3068 y Fl(;)10 b Fe(h)2093 3077 y Fh(2)2117 3068 y Fp(g)p Fo(\))15 b Fe(does)0 3140 y(not.)0 3278 y Fd(Example)f(8.17)29 b Fe(Skip)12 b Fk(#)h Fe(Skip)j Fo(=)g Fe(Skip)1118 3427 y Ff(51)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF -- A E Lawrence, MA., DPhil. adrian.lawrence@oucs.ox.ac.uk. MicroProcessor Unit, 13, Banbury Road, Oxford. OX2 6NN. UK. Voice: (+44)-1865-273274, Fax: (+44)-1865-273275