source: vis_dev/vis-2.1/doc/ctl.ps @ 12

%!PS-Adobe-2.0
%%Creator: dvipsk 5.58a Copyright 1986, 1994 Radical Eye Software
%%Title: ctl.dvi
%%Pages: 3
%%PageOrder: Ascend
%%BoundingBox: 0 0 596 842
%%DocumentFonts: Times-Roman Times-Italic Courier Times-Bold
%%DocumentPaperSizes: a4
%%EndComments
%DVIPSCommandLine: dvips ctl.dvi -o ctl.ps
%DVIPSParameters: dpi=300, compressed, comments removed
%DVIPSSource:  TeX output 1997.02.27:1204
%%BeginProcSet: texc.pro
/TeXDict 250 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 0 1 255{IE S 1 string dup 0 3 index put cvn put}for
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 product dup length 7 ge{0 7
getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false}
ifelse}{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: 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 load]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 300 300 (ctl.dvi)
@start /Fa 1 107 df<12C0B3AF02217C980A>106 D E /Fb 134[17
2[17 17 9 13 11 1[17 17 17 1[9 2[9 2[11 15 17 15 1[15
14[22 2[24 24 9[24 2[24 18[8 7[26 38[{}23 33.333334 /Times-Roman
rf /Fc 1 50 df<1218127812981218AC12FF08107D8F0F>49 D
E /Fd 81[33 57[20 23 27 2[30 33 50 17 2[17 33 2[27 1[27
33 30 10[43 7[43 56 4[47 3[43 68[{}19 59.999974 /Times-Bold
rf /Fe 1 50 df<120C121C12EC120CAFEAFFC00A137D9211>49
D E /Ff 59[25 25 69[25 25 25 25 25 25 1[25 25 25 25 25
1[25 25 25 25 25 25 25 25 25 25 25 25 25 25 25 25 1[25
1[25 25 25 25 25 25 1[25 25 25 1[25 25 25 25 25 25 25
2[25 1[25 25 25 25 25 25 25 25 25 25 25 25 25 25 25 6[25
25 25 25 25 25 25 25 25 25 25 25 1[25 25 25 25 25 33[{}79
41.666669 /Courier rf /Fg 81[21 52[18 2[18 21 12 16 16
1[21 21 21 30 12 2[12 1[21 12 18 1[18 21 21 10[25 30
23 21 6[23 5[25 2[28 1[25 3[28 10[21 21 3[14 45[{}31
41.666669 /Times-Italic rf /Fh 69[18 11[23 52[21 21 30
21 21 12 16 14 21 21 21 21 32 12 21 12 12 21 21 14 18
21 18 21 18 14 2[14 1[14 1[30 1[39 30 30 25 23 28 1[23
30 30 37 25 2[14 30 30 23 25 30 28 28 30 38 2[23 1[12
12 21 21 21 21 1[21 21 21 21 21 1[10 14 10 2[14 14 14
39[{}70 41.666669 /Times-Roman rf /Fi 5 123 df<00C0130214060060130CA26C
1318A36C1330A26C1360A26C13C0A338030180A238018300A2EA00C6A2136CA31338A213
10171A7E981C>95 D<133C13E0EA01C013801203AD13005A121C12F0121C12077E1380AD
120113C0EA00E0133C0E297D9E15>102 D<12F0121C12077E1380AD120113C0EA00E013
3C13E0EA01C013801203AD13005A121C12F00E297D9E15>I<12021207A61202A3EA7270
EAFFF8EA7270EA0200A21207B11202A60D267E9C12>121 D<12021207A41202A2EA4210
EAFFF8A2EA0200A31207A41202C7FC12021207A41202A3EAFFF8A2EA4210EA0200A21207
A412020D257E9C12>I E /Fj 2 123 df<5AEA0380A7EA0100A5EA793CEAFFFEEA793CEA
0100A3EA0380B3A2EA0100A70F2E7DA216>121 D<5AEA0380A5EA0100A3EA4104EAFFFE
A2EA0100A4EA0380A5EA0100C7FC5AEA0380A5EA0100A4EAFFFEA2EA4104EA0100A3EA03
80A5EA01000F2D7DA216>I E /Fk 134[25 3[25 14 1[17 2[25
25 39 1[25 14 14 1[25 1[22 2[25 22 7[36 13[36 19 3[28
12[25 1[25 4[25 25 3[17 12 44[{}24 50.000001 /Times-Roman
rf /Fl 134[36 36 3[20 5[36 12[32 10[52 1[44 40 6[44 2[24
5[48 67[{}11 71.999998 /Times-Roman rf end
%%EndProlog
%%BeginSetup
%%Feature: *Resolution 300dpi
TeXDict begin
%%PaperSize: a4
%%BeginPaperSize: a4
a4
%%EndPaperSize

%%EndSetup
%%Page: 1 1
1 0 bop 734 482 a Fl(VIS)18 b(CTL)f(Syntax)724 602 y
Fk(Y)-6 b(uji)12 b(Kukimoto)p Fj(y)49 b Fk(Jae-Y)-5 b(oung)12
b(Jang)p Fj(z)533 690 y Fi(y)f Fh(The)g(VIS)f(Group)392
739 y(University)e(of)i(California,)f(Berkeley)467 789
y(vis@ic.eecs.berkeley)m(.edu)1323 690 y Fi(z)i Fh(The)g(VIS)f(Group)
1197 739 y(University)f(of)h(Colorado,)f(Boulder)1257
789 y(vis@ic.eecs.berkeley)m(.edu)794 919 y Fk(February)j(27,)g(1997)
324 1065 y Fh(CTL)c(\(Computation)d(T)o(ree)j(Logic\))f(is)g(a)h
(language)g(used)f(to)g(describe)h(properties)f(of)g(systems.)262
1115 y(This)12 b(document)f(describes)i(the)f(CTL)h(syntax)e(used)i(in)
e(VIS.)h(For)g(the)g(semantics)h(of)f(CTL,)h(the)262
1164 y(reader)e(should)e(refer)h(to)g(the)g(following)e(paper)n(.)365
1248 y(E.)15 b(M.)f(Clarke,)i(E.)e(A.)h(Emerson)f(and)g(A.)h(P)-5
b(.)15 b(Sistla,)f Fg(Automatic)f(V)-5 b(eri\256cation)14
b(of)365 1297 y(Finite-State)5 b(Concurr)n(ent)i(Systems)g(Using)f(T)l
(emporal)h(Logic)g(Speci\256cations)p Fh(,)f(ACM)365
1347 y(T)o(ransactions)h(on)g(Programming)f(Languages)i(and)g(Systems,)
g(vol)e(8-2,)i(pages)g(244-)365 1397 y(263,)i(April,)g(1986)324
1480 y(This)g(syntax)g(should)g(be)h(followed)e(when)h(VIS)h(users)g
(create)h(CTL)f(\256les)g(and)f(fairness)h(con-)262 1530
y(straint)f(\256les)i(for)f(the)g(commands)i Ff(model)p
899 1530 13 2 v 14 w(check)p Fh(,)f Ff(approximate)p
1335 1530 V 14 w(model)p 1474 1530 V 15 w(check)p Fh(,)g(and)262
1580 y Ff(read)p 364 1580 V 14 w(fairness)p Fh(,)e(respectively)m(.)324
1630 y(The)h(syntax)e(for)h(CTL)h(is:)365 1706 y(TRUE,)h(F)m(ALSE,)g
(and)f Fg(var)o(-name=value)h Fh(are)f(CTL)h(formulas,)f(where)h
Fg(var)o(-name)365 1756 y Fh(is)e(the)h(full)e(hierarchical)h(name)h
(of)f(a)h(variable,)f(and)h Fg(value)f Fh(is)g(a)h(legal)f(value)g(in)g
(the)365 1806 y(domain)i(of)h(the)f(variable.)20 b Fg(var)o(-name1)13
b(==)g(var)o(-name2)f Fh(is)h(the)f(atomic)g(formula)365
1856 y(that)d(is)f(true)h(if)f Fg(var)o(-name1)h Fh(has)g(the)g(same)h
(value)f(as)g Fg(var)o(-name2)p Fh(.)14 b(Currently)7
b(it)h(can)365 1905 y(be)14 b(used)f(only)f(in)h(the)g(Boolean)f
(domain.)22 b(\(It)13 b(cannot)g(be)g(used)h(for)e(variables)h(of)365
1955 y(enumerated)h(types.\))24 b Fg(var)o(-name1)p Fh([i:j])11
b(==)k Fg(var)o(-name2)p Fh([k:l])d(can)i(be)g(used)f(if)g(the)365
2005 y(lengths)e(of)h(vectors)g(are)h(the)f(same.)21
b(V)-5 b(ector)12 b(variables,)h(the)f(syntax)f(of)h(hierarch-)365
2055 y(ical)e(names,)h(and)f(macro)g(de\256nition)e(are)j(described)e
(later)h(in)f(this)g(document.)k(The)365 2105 y(following)8
b(character)k(set)e(may)h(be)f(used)h(for)f(variable)g(names)h(and)g
(values:)365 2203 y Ff(A-Z)25 b(a-z)g(0-9)f(\303)h(?)g(|)g(/)f([)h(])g
(+)g(*)g($)f(<)h(>)g(\304)g(@)g(_)g(#)f(\045)h(:)g(")g(')g(.)365
2301 y Fh(If)10 b(f)h(and)f(g)g(are)h(CTL)g(formulas,)f(then)g(so)g
(are)h(the)f(following:)365 2399 y Ff(\(f\),)25 b(f)g(*)f(g,)h(f)g(+)g
(g,)g(f)f(\303)h(g,)g(!f,)f(f)h(->)g(g,)g(f)g(<->)f(g,)h(AG)g(f,)365
2449 y(AF)g(f,)g(AX)f(f,)h(EG)g(f,)g(EF)f(f,)h(EX)g(f,)f(A\(f)h(U)g
(g\))g(and)f(E\(f)h(U)g(g\).)967 2574 y Fh(1)p eop
%%Page: 2 2
2 1 bop 365 307 a Ff(AX:n\(f\))7 b Fh(is)f(allowed)h(as)g(a)g
(shorthand)f(for)g Ff(AX\(AX\(...AX\(f\)...\)\))p Fh(,)h(where)365
357 y Ff(n)k Fh(is)f(the)g(number)g(of)g(invocations)f(of)h
Ff(AX)p Fh(.)g Ff(EX:n\(f\))g Fh(is)g(de\256ned)h(similarly)m(.)365
421 y(Binary)f(operators)g(must)g(be)g(surrounded)g(by)g(spaces,)i
(i.e.)j Ff(f)24 b(+)h(g)11 b Fh(is)f(a)h(CTL)f(for)o(-)365
471 y(mula)g(while)e Ff(f+g)h Fh(is)g(not.)k(The)d(same)h(is)e(true)g
(for)f Ff(U)h Fh(in)g(until)f(formulas.)13 b(Once)d(par)o(-)365
521 y(entheses)i(are)h(inserted,)e(the)g(spaces)i(can)f(be)g(omitted,)f
(i.e.)18 b Ff(\(f\)+\(g\))11 b Fh(is)g(a)h(valid)365
571 y(formula.)i(Unary)9 b(temporal)h(operators)f(and)h(their)f(ar)o
(guments)h(must)f(be)h(separated)365 620 y(by)g(spaces)i(unless)e
(parentheses)h(are)g(used.)365 685 y(The)g(symbols)f(have)h(the)f
(following)e(meanings)1070 670 y Fe(1)1088 685 y Fh(.)365
780 y Ff(*)25 b(--)g(AND,)f(+)h(--)g(OR,)g(\303)f(--)h(XOR,)g(!)f(--)h
(NOT,)g(->)f(--)h(IMPLY,)365 829 y(<->)g(--)g(EQUIV)365
924 y Fh(Operator)10 b(Precedence:)365 988 y(High)465
1083 y Ff(!)465 1183 y(AG,)25 b(AF,)f(AX,)h(EG,)f(EF,)h(EX)465
1282 y(*)465 1382 y(+)465 1482 y(\303)465 1581 y(<->)465
1681 y(->)465 1781 y(U)365 1875 y Fh(Low)324 1950 y(An)12
b(entire)g(formula)f(should)g(be)i(followed)d(by)i(a)h(semicolon.)19
b(All)12 b(text)f(from)h Ff(#)g Fh(to)g(the)g(end)262
2000 y(of)f(a)i(line)f(is)f(treated)i(as)f(a)h(comment.)20
b(The)13 b(model)f(checker)i(\()p Ff(mc)p Fh(\))d(package)j(is)d(used)i
(to)e(decide)262 2049 y(whether)h(or)f(not)h(a)h(given)e(FSM)h
(satis\256es)h(a)g(given)e(CTL)i(formula.)20 b(See)13
b(the)f(help)g(\256les)g(for)g(the)262 2099 y Ff(model)p
389 2099 13 2 v 14 w(check)e Fh(and)g Ff(approximate)p
883 2099 V 14 w(model)p 1022 2099 V 15 w(check)g Fh(commands)h(for)f
(more)g(details.)262 2237 y Fd(Hierar)o(chi)o(cal)h(Names)262
2330 y Fh(If)e(a)h(variable)f Fg(var)h Fh(belongs)f(to)g(the)g(root)g
(model,)h(the)f(hierarchical)h(name)h(of)e(the)g(variable)h(is)f
Fg(var)p Fh(.)262 2379 y(If)j(the)g(variable)h(belongs)e(to)h(a)h
(subcircuit)f(in)g(the)g(root)g(model,)h(the)g(hierarchical)f(name)i
(of)e(the)p 262 2411 573 2 v 304 2437 a Fc(1)321 2449
y Fb(&&)c(and)g Fa(jj)f Fb(are)h(also)g(supported)e(for)i(AND)h(and)e
(OR)h(respectively)n(.)967 2574 y Fh(2)p eop
%%Page: 3 3
3 2 bop 262 307 a Fh(variable)7 b(is)h Fg(subcir)n(cuit)p
606 307 13 2 v 14 w(name)p Fh(.)p Fg(var)p Fh(,)h(where)g
Fg(subcir)n(cuit)p 1069 307 V 14 w(name)f Fh(is)g(the)f(name)i(of)e
(the)h(subcircuit.)k(In)262 357 y(general,)d(the)f(hierarchical)g(name)
i(of)e(a)h(variable)f(is)g(the)g(names)i(of)e(the)g(subcircuits)f
(concatenated)262 407 y(with)i(`.')14 b(followed)8 b(by)i(its)g(name.)
262 547 y Fd(V)-5 b(ector)13 b(V)-5 b(ariables)262 639
y Fh(V)g(ector)7 b(variables)g(have)g(the)g(form)f Fg(var)o(-name)p
Fh([i:j];)g(each)i(bit)e(can)i(be)f(written)e(as)j(either)e
Fg(var)o(-name)p Ff(<)p Fh(i)p Ff(>)262 689 y Fh(or)j
Fg(var)o(-name)p Fh([i].)14 b(T)m(o)d(compare)g(a)g Fg(value)f
Fh(to)g(a)h Fg(vector)g(variable)p Fh(,)f(the)g(following)e(can)j(be)f
(used.)262 772 y Ff(var-name[i:j])23 b(=)i(n)610 822
y(=)g(bxxx)610 872 y(=)g({value1,value2,...,valueN})262
971 y(n:)f(integer,)g(bxxx:)h(binary)f(string,)g(valueN:)h(either)f(n)h
(or)g(bxxx)262 1054 y Fh(For)7 b(instance,)i(counter[3:0])d(=)j(10,)f
(counter[3:0])e(=)j(b1010,)e(counter[3:0])f(=)j Fi(f)p
Fh(1,2,10)p Fi(g)e Fh(are)i(valid)262 1104 y(formulae.)17
b(For)11 b(variables)h(of)f(enumerated)h(types,)g(one)g(can)g(write)f
Fg(var)o(-name)g Fh(=)h Fi(f)p Fh(RED,)g(YEL-)262 1154
y(LOW)l(,)f(BLUE)p Fi(g)g Fh(without)d(vector)i(indices.)k
Fg(var)o(-name)p Fh([i:j])9 b(=)i Fi(f)p Fh(value1,value2,...,valueN)p
Fi(g)h Fh(rep-)262 1204 y(resents)7 b(set)g(membership;)h(that)e(is,)i
(it)e(is)g(equivalent)g(to)g(\()p Fg(var)o(-name)p Fh([i:j])f(=)j
(value1\))e Fi(_)h Fh(\()p Fg(var)o(-name)p Fh([i:j])262
1254 y(=)j(value2\))g Fi(_)g Fh(...)15 b Fi(_)10 b Fh(\()p
Fg(var)o(-name)p Fh([i:j])f(=)i(valueN\).)262 1393 y
Fd(Macr)o(o)j(De\256nition)262 1486 y Fh(Macros)d(can)h(be)f(de\256ned)
h(and)f(used)g(in)g(CTL)g(formulae)h(for)e(valid)g(sub-formulae.)16
b(Y)l(ou)11 b(cannot)262 1536 y(use)e(a)g(macro)h(such)f(as)h(\272)p
Ff(\\)p Fh(de\256ne)g(MSB)f(7\272)g(since)g(\2727\272)h(is)f(not)f(a)h
(valid)g(CTL)g(formula.)k(The)d(macro)262 1586 y(de\256nition)e(must)i
(precede)i(its)d(use.)262 1669 y Ff({\\DEFINE)24 b(|)g(\\Define)h(|)g
(\\define})f(MACRO)g(formula)262 1752 y Fh(For)10 b(instance,)262
1835 y Ff(\\define)24 b(Red)g(t_sig)h(=)g(RED)262 1884
y(\\define)f(Blue)g(t_sig)h(=)g(BLUE)262 1967 y Fh(de\256nes)11
b Ff(\\Red)f Fh(as)h(a)g(shorthand)e(for)h Ff(t_sig)24
b(=)h(RED)p Fh(.)11 b(Similarly)e(for)g Ff(\\Blue)p Fh(.)14
b(One)d(can)g(then)262 2017 y(write:)262 2100 y Ff(AG)24
b(\()h(\\Red)g(->)f(AX)h(\()g(\\Blue)f(\))h(\);)967 2574
y Fh(3)p eop
%%Trailer
end
userdict /end-hook known{end-hook}if
%%EOF