[14] | 1 | %!PS-Adobe-2.0 |
---|
| 2 | %%Creator: dvipsk 5.58a Copyright 1986, 1994 Radical Eye Software |
---|
| 3 | %%Title: ctl.dvi |
---|
| 4 | %%Pages: 3 |
---|
| 5 | %%PageOrder: Ascend |
---|
| 6 | %%BoundingBox: 0 0 596 842 |
---|
| 7 | %%DocumentFonts: Times-Roman Times-Italic Courier Times-Bold |
---|
| 8 | %%DocumentPaperSizes: a4 |
---|
| 9 | %%EndComments |
---|
| 10 | %DVIPSCommandLine: dvips ctl.dvi -o ctl.ps |
---|
| 11 | %DVIPSParameters: dpi=300, compressed, comments removed |
---|
| 12 | %DVIPSSource: TeX output 1997.02.27:1204 |
---|
| 13 | %%BeginProcSet: texc.pro |
---|
| 14 | /TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N |
---|
| 15 | /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 |
---|
| 16 | mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} |
---|
| 17 | ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale |
---|
| 18 | isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div |
---|
| 19 | hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul |
---|
| 20 | TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if} |
---|
| 21 | forall round exch round exch]setmatrix}N /@landscape{/isls true N}B |
---|
| 22 | /@manualfeed{statusdict /manualfeed true put}B /@copies{/#copies X}B |
---|
| 23 | /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{ |
---|
| 24 | /nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N |
---|
| 25 | string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N |
---|
| 26 | end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{ |
---|
| 27 | /sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0] |
---|
| 28 | N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup |
---|
| 29 | length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{ |
---|
| 30 | 128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub |
---|
| 31 | get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data |
---|
| 32 | dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N |
---|
| 33 | /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup |
---|
| 34 | /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx |
---|
| 35 | 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff |
---|
| 36 | setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff |
---|
| 37 | .1 sub]/id ch-image N /rw ch-width 7 add 8 idiv string N /rc 0 N /gp 0 N |
---|
| 38 | /cp 0 N{rc 0 ne{rc 1 sub /rc X rw}{G}ifelse}imagemask restore}B /G{{id |
---|
| 39 | gp get /gp gp 1 add N dup 18 mod S 18 idiv pl S get exec}loop}B /adv{cp |
---|
| 40 | add /cp X}B /chg{rw cp id gp 4 index getinterval putinterval dup gp add |
---|
| 41 | /gp X adv}B /nd{/cp 0 N rw exit}B /lsh{rw cp 2 copy get dup 0 eq{pop 1}{ |
---|
| 42 | dup 255 eq{pop 254}{dup dup add 255 and S 1 and or}ifelse}ifelse put 1 |
---|
| 43 | adv}B /rsh{rw cp 2 copy get dup 0 eq{pop 128}{dup 255 eq{pop 127}{dup 2 |
---|
| 44 | idiv S 128 and or}ifelse}ifelse put 1 adv}B /clr{rw cp 2 index string |
---|
| 45 | putinterval adv}B /set{rw cp fillstr 0 4 index getinterval putinterval |
---|
| 46 | adv}B /fillstr 18 string 0 1 17{2 copy 255 put pop}for N /pl[{adv 1 chg} |
---|
| 47 | {adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{ |
---|
| 48 | adv rsh nd}{1 add adv}{/rc X nd}{1 add set}{1 add clr}{adv 2 chg}{adv 2 |
---|
| 49 | chg nd}{pop nd}]dup{bind pop}forall N /D{/cc X dup type /stringtype ne{] |
---|
| 50 | }if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup |
---|
| 51 | length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{ |
---|
| 52 | cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin |
---|
| 53 | 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul |
---|
| 54 | add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore userdict |
---|
| 55 | /eop-hook known{eop-hook}if showpage}N /@start{userdict /start-hook |
---|
| 56 | known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X |
---|
| 57 | /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for |
---|
| 58 | 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 |
---|
| 59 | 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V |
---|
| 60 | {}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7 |
---|
| 61 | getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false} |
---|
| 62 | ifelse}{false}ifelse end{{gsave TR -.1 .1 TR 1 1 scale rulex ruley false |
---|
| 63 | RMat{BDot}imagemask grestore}}{{gsave TR -.1 .1 TR rulex ruley scale 1 1 |
---|
| 64 | false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave newpath transform |
---|
| 65 | round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg |
---|
| 66 | rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail |
---|
| 67 | {dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}B /c{-4 M} |
---|
| 68 | 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{ |
---|
| 69 | 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{ |
---|
| 70 | 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 |
---|
| 71 | a}B /bos{/SS save N}B /eos{SS restore}B end |
---|
| 72 | %%EndProcSet |
---|
| 73 | %%BeginProcSet: texps.pro |
---|
| 74 | TeXDict begin /rf{findfont dup length 1 add dict begin{1 index /FID ne 2 |
---|
| 75 | index /UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll |
---|
| 76 | exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics |
---|
| 77 | exch def dict begin Encoding{exch dup type /integertype ne{pop pop 1 sub |
---|
| 78 | dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def} |
---|
| 79 | ifelse}forall Metrics /Metrics currentdict end def[2 index currentdict |
---|
| 80 | end definefont 3 -1 roll makefont /setfont load]cvx def}def |
---|
| 81 | /ObliqueSlant{dup sin S cos div neg}B /SlantFont{4 index mul add}def |
---|
| 82 | /ExtendFont{3 -1 roll mul exch}def /ReEncodeFont{/Encoding exch def}def |
---|
| 83 | end |
---|
| 84 | %%EndProcSet |
---|
| 85 | TeXDict begin 39158280 55380996 1000 300 300 (ctl.dvi) |
---|
| 86 | @start /Fa 1 107 df<12C0B3AF02217C980A>106 D E /Fb 134[17 |
---|
| 87 | 2[17 17 9 13 11 1[17 17 17 1[9 2[9 2[11 15 17 15 1[15 |
---|
| 88 | 14[22 2[24 24 9[24 2[24 18[8 7[26 38[{}23 33.333334 /Times-Roman |
---|
| 89 | rf /Fc 1 50 df<1218127812981218AC12FF08107D8F0F>49 D |
---|
| 90 | E /Fd 81[33 57[20 23 27 2[30 33 50 17 2[17 33 2[27 1[27 |
---|
| 91 | 33 30 10[43 7[43 56 4[47 3[43 68[{}19 59.999974 /Times-Bold |
---|
| 92 | rf /Fe 1 50 df<120C121C12EC120CAFEAFFC00A137D9211>49 |
---|
| 93 | D E /Ff 59[25 25 69[25 25 25 25 25 25 1[25 25 25 25 25 |
---|
| 94 | 1[25 25 25 25 25 25 25 25 25 25 25 25 25 25 25 25 1[25 |
---|
| 95 | 1[25 25 25 25 25 25 1[25 25 25 1[25 25 25 25 25 25 25 |
---|
| 96 | 2[25 1[25 25 25 25 25 25 25 25 25 25 25 25 25 25 25 6[25 |
---|
| 97 | 25 25 25 25 25 25 25 25 25 25 25 1[25 25 25 25 25 33[{}79 |
---|
| 98 | 41.666669 /Courier rf /Fg 81[21 52[18 2[18 21 12 16 16 |
---|
| 99 | 1[21 21 21 30 12 2[12 1[21 12 18 1[18 21 21 10[25 30 |
---|
| 100 | 23 21 6[23 5[25 2[28 1[25 3[28 10[21 21 3[14 45[{}31 |
---|
| 101 | 41.666669 /Times-Italic rf /Fh 69[18 11[23 52[21 21 30 |
---|
| 102 | 21 21 12 16 14 21 21 21 21 32 12 21 12 12 21 21 14 18 |
---|
| 103 | 21 18 21 18 14 2[14 1[14 1[30 1[39 30 30 25 23 28 1[23 |
---|
| 104 | 30 30 37 25 2[14 30 30 23 25 30 28 28 30 38 2[23 1[12 |
---|
| 105 | 12 21 21 21 21 1[21 21 21 21 21 1[10 14 10 2[14 14 14 |
---|
| 106 | 39[{}70 41.666669 /Times-Roman rf /Fi 5 123 df<00C0130214060060130CA26C |
---|
| 107 | 1318A36C1330A26C1360A26C13C0A338030180A238018300A2EA00C6A2136CA31338A213 |
---|
| 108 | 10171A7E981C>95 D<133C13E0EA01C013801203AD13005A121C12F0121C12077E1380AD |
---|
| 109 | 120113C0EA00E0133C0E297D9E15>102 D<12F0121C12077E1380AD120113C0EA00E013 |
---|
| 110 | 3C13E0EA01C013801203AD13005A121C12F00E297D9E15>I<12021207A61202A3EA7270 |
---|
| 111 | EAFFF8EA7270EA0200A21207B11202A60D267E9C12>121 D<12021207A41202A2EA4210 |
---|
| 112 | EAFFF8A2EA0200A31207A41202C7FC12021207A41202A3EAFFF8A2EA4210EA0200A21207 |
---|
| 113 | A412020D257E9C12>I E /Fj 2 123 df<5AEA0380A7EA0100A5EA793CEAFFFEEA793CEA |
---|
| 114 | 0100A3EA0380B3A2EA0100A70F2E7DA216>121 D<5AEA0380A5EA0100A3EA4104EAFFFE |
---|
| 115 | A2EA0100A4EA0380A5EA0100C7FC5AEA0380A5EA0100A4EAFFFEA2EA4104EA0100A3EA03 |
---|
| 116 | 80A5EA01000F2D7DA216>I E /Fk 134[25 3[25 14 1[17 2[25 |
---|
| 117 | 25 39 1[25 14 14 1[25 1[22 2[25 22 7[36 13[36 19 3[28 |
---|
| 118 | 12[25 1[25 4[25 25 3[17 12 44[{}24 50.000001 /Times-Roman |
---|
| 119 | rf /Fl 134[36 36 3[20 5[36 12[32 10[52 1[44 40 6[44 2[24 |
---|
| 120 | 5[48 67[{}11 71.999998 /Times-Roman rf end |
---|
| 121 | %%EndProlog |
---|
| 122 | %%BeginSetup |
---|
| 123 | %%Feature: *Resolution 300dpi |
---|
| 124 | TeXDict begin |
---|
| 125 | %%PaperSize: a4 |
---|
| 126 | %%BeginPaperSize: a4 |
---|
| 127 | a4 |
---|
| 128 | %%EndPaperSize |
---|
| 129 | |
---|
| 130 | %%EndSetup |
---|
| 131 | %%Page: 1 1 |
---|
| 132 | 1 0 bop 734 482 a Fl(VIS)18 b(CTL)f(Syntax)724 602 y |
---|
| 133 | Fk(Y)-6 b(uji)12 b(Kukimoto)p Fj(y)49 b Fk(Jae-Y)-5 b(oung)12 |
---|
| 134 | b(Jang)p Fj(z)533 690 y Fi(y)f Fh(The)g(VIS)f(Group)392 |
---|
| 135 | 739 y(University)e(of)i(California,)f(Berkeley)467 789 |
---|
| 136 | y(vis@ic.eecs.berkeley)m(.edu)1323 690 y Fi(z)i Fh(The)g(VIS)f(Group) |
---|
| 137 | 1197 739 y(University)f(of)h(Colorado,)f(Boulder)1257 |
---|
| 138 | 789 y(vis@ic.eecs.berkeley)m(.edu)794 919 y Fk(February)j(27,)g(1997) |
---|
| 139 | 324 1065 y Fh(CTL)c(\(Computation)d(T)o(ree)j(Logic\))f(is)g(a)h |
---|
| 140 | (language)g(used)f(to)g(describe)h(properties)f(of)g(systems.)262 |
---|
| 141 | 1115 y(This)12 b(document)f(describes)i(the)f(CTL)h(syntax)e(used)i(in) |
---|
| 142 | e(VIS.)h(For)g(the)g(semantics)h(of)f(CTL,)h(the)262 |
---|
| 143 | 1164 y(reader)e(should)e(refer)h(to)g(the)g(following)e(paper)n(.)365 |
---|
| 144 | 1248 y(E.)15 b(M.)f(Clarke,)i(E.)e(A.)h(Emerson)f(and)g(A.)h(P)-5 |
---|
| 145 | b(.)15 b(Sistla,)f Fg(Automatic)f(V)-5 b(eri\256cation)14 |
---|
| 146 | b(of)365 1297 y(Finite-State)5 b(Concurr)n(ent)i(Systems)g(Using)f(T)l |
---|
| 147 | (emporal)h(Logic)g(Speci\256cations)p Fh(,)f(ACM)365 |
---|
| 148 | 1347 y(T)o(ransactions)h(on)g(Programming)f(Languages)i(and)g(Systems,) |
---|
| 149 | g(vol)e(8-2,)i(pages)g(244-)365 1397 y(263,)i(April,)g(1986)324 |
---|
| 150 | 1480 y(This)g(syntax)g(should)g(be)h(followed)e(when)h(VIS)h(users)g |
---|
| 151 | (create)h(CTL)f(\256les)g(and)f(fairness)h(con-)262 1530 |
---|
| 152 | y(straint)f(\256les)i(for)f(the)g(commands)i Ff(model)p |
---|
| 153 | 899 1530 13 2 v 14 w(check)p Fh(,)f Ff(approximate)p |
---|
| 154 | 1335 1530 V 14 w(model)p 1474 1530 V 15 w(check)p Fh(,)g(and)262 |
---|
| 155 | 1580 y Ff(read)p 364 1580 V 14 w(fairness)p Fh(,)e(respectively)m(.)324 |
---|
| 156 | 1630 y(The)h(syntax)e(for)h(CTL)h(is:)365 1706 y(TRUE,)h(F)m(ALSE,)g |
---|
| 157 | (and)f Fg(var)o(-name=value)h Fh(are)f(CTL)h(formulas,)f(where)h |
---|
| 158 | Fg(var)o(-name)365 1756 y Fh(is)e(the)h(full)e(hierarchical)h(name)h |
---|
| 159 | (of)f(a)h(variable,)f(and)h Fg(value)f Fh(is)g(a)h(legal)f(value)g(in)g |
---|
| 160 | (the)365 1806 y(domain)i(of)h(the)f(variable.)20 b Fg(var)o(-name1)13 |
---|
| 161 | b(==)g(var)o(-name2)f Fh(is)h(the)f(atomic)g(formula)365 |
---|
| 162 | 1856 y(that)d(is)f(true)h(if)f Fg(var)o(-name1)h Fh(has)g(the)g(same)h |
---|
| 163 | (value)f(as)g Fg(var)o(-name2)p Fh(.)14 b(Currently)7 |
---|
| 164 | b(it)h(can)365 1905 y(be)14 b(used)f(only)f(in)h(the)g(Boolean)f |
---|
| 165 | (domain.)22 b(\(It)13 b(cannot)g(be)g(used)h(for)e(variables)h(of)365 |
---|
| 166 | 1955 y(enumerated)h(types.\))24 b Fg(var)o(-name1)p Fh([i:j])11 |
---|
| 167 | b(==)k Fg(var)o(-name2)p Fh([k:l])d(can)i(be)g(used)f(if)g(the)365 |
---|
| 168 | 2005 y(lengths)e(of)h(vectors)g(are)h(the)f(same.)21 |
---|
| 169 | b(V)-5 b(ector)12 b(variables,)h(the)f(syntax)f(of)h(hierarch-)365 |
---|
| 170 | 2055 y(ical)e(names,)h(and)f(macro)g(de\256nition)e(are)j(described)e |
---|
| 171 | (later)h(in)f(this)g(document.)k(The)365 2105 y(following)8 |
---|
| 172 | b(character)k(set)e(may)h(be)f(used)h(for)f(variable)g(names)h(and)g |
---|
| 173 | (values:)365 2203 y Ff(A-Z)25 b(a-z)g(0-9)f(\303)h(?)g(|)g(/)f([)h(])g |
---|
| 174 | (+)g(*)g($)f(<)h(>)g(\304)g(@)g(_)g(#)f(\045)h(:)g(")g(')g(.)365 |
---|
| 175 | 2301 y Fh(If)10 b(f)h(and)f(g)g(are)h(CTL)g(formulas,)f(then)g(so)g |
---|
| 176 | (are)h(the)f(following:)365 2399 y Ff(\(f\),)25 b(f)g(*)f(g,)h(f)g(+)g |
---|
| 177 | (g,)g(f)f(\303)h(g,)g(!f,)f(f)h(->)g(g,)g(f)g(<->)f(g,)h(AG)g(f,)365 |
---|
| 178 | 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 |
---|
| 179 | (g\))g(and)f(E\(f)h(U)g(g\).)967 2574 y Fh(1)p eop |
---|
| 180 | %%Page: 2 2 |
---|
| 181 | 2 1 bop 365 307 a Ff(AX:n\(f\))7 b Fh(is)f(allowed)h(as)g(a)g |
---|
| 182 | (shorthand)f(for)g Ff(AX\(AX\(...AX\(f\)...\)\))p Fh(,)h(where)365 |
---|
| 183 | 357 y Ff(n)k Fh(is)f(the)g(number)g(of)g(invocations)f(of)h |
---|
| 184 | Ff(AX)p Fh(.)g Ff(EX:n\(f\))g Fh(is)g(de\256ned)h(similarly)m(.)365 |
---|
| 185 | 421 y(Binary)f(operators)g(must)g(be)g(surrounded)g(by)g(spaces,)i |
---|
| 186 | (i.e.)j Ff(f)24 b(+)h(g)11 b Fh(is)f(a)h(CTL)f(for)o(-)365 |
---|
| 187 | 471 y(mula)g(while)e Ff(f+g)h Fh(is)g(not.)k(The)d(same)h(is)e(true)g |
---|
| 188 | (for)f Ff(U)h Fh(in)g(until)f(formulas.)13 b(Once)d(par)o(-)365 |
---|
| 189 | 521 y(entheses)i(are)h(inserted,)e(the)g(spaces)i(can)f(be)g(omitted,)f |
---|
| 190 | (i.e.)18 b Ff(\(f\)+\(g\))11 b Fh(is)g(a)h(valid)365 |
---|
| 191 | 571 y(formula.)i(Unary)9 b(temporal)h(operators)f(and)h(their)f(ar)o |
---|
| 192 | (guments)h(must)f(be)h(separated)365 620 y(by)g(spaces)i(unless)e |
---|
| 193 | (parentheses)h(are)g(used.)365 685 y(The)g(symbols)f(have)h(the)f |
---|
| 194 | (following)e(meanings)1070 670 y Fe(1)1088 685 y Fh(.)365 |
---|
| 195 | 780 y Ff(*)25 b(--)g(AND,)f(+)h(--)g(OR,)g(\303)f(--)h(XOR,)g(!)f(--)h |
---|
| 196 | (NOT,)g(->)f(--)h(IMPLY,)365 829 y(<->)g(--)g(EQUIV)365 |
---|
| 197 | 924 y Fh(Operator)10 b(Precedence:)365 988 y(High)465 |
---|
| 198 | 1083 y Ff(!)465 1183 y(AG,)25 b(AF,)f(AX,)h(EG,)f(EF,)h(EX)465 |
---|
| 199 | 1282 y(*)465 1382 y(+)465 1482 y(\303)465 1581 y(<->)465 |
---|
| 200 | 1681 y(->)465 1781 y(U)365 1875 y Fh(Low)324 1950 y(An)12 |
---|
| 201 | b(entire)g(formula)f(should)g(be)i(followed)d(by)i(a)h(semicolon.)19 |
---|
| 202 | b(All)12 b(text)f(from)h Ff(#)g Fh(to)g(the)g(end)262 |
---|
| 203 | 2000 y(of)f(a)i(line)f(is)f(treated)i(as)f(a)h(comment.)20 |
---|
| 204 | b(The)13 b(model)f(checker)i(\()p Ff(mc)p Fh(\))d(package)j(is)d(used)i |
---|
| 205 | (to)e(decide)262 2049 y(whether)h(or)f(not)h(a)h(given)e(FSM)h |
---|
| 206 | (satis\256es)h(a)g(given)e(CTL)i(formula.)20 b(See)13 |
---|
| 207 | b(the)f(help)g(\256les)g(for)g(the)262 2099 y Ff(model)p |
---|
| 208 | 389 2099 13 2 v 14 w(check)e Fh(and)g Ff(approximate)p |
---|
| 209 | 883 2099 V 14 w(model)p 1022 2099 V 15 w(check)g Fh(commands)h(for)f |
---|
| 210 | (more)g(details.)262 2237 y Fd(Hierar)o(chi)o(cal)h(Names)262 |
---|
| 211 | 2330 y Fh(If)e(a)h(variable)f Fg(var)h Fh(belongs)f(to)g(the)g(root)g |
---|
| 212 | (model,)h(the)f(hierarchical)h(name)h(of)e(the)g(variable)h(is)f |
---|
| 213 | Fg(var)p Fh(.)262 2379 y(If)j(the)g(variable)h(belongs)e(to)h(a)h |
---|
| 214 | (subcircuit)f(in)g(the)g(root)g(model,)h(the)g(hierarchical)f(name)i |
---|
| 215 | (of)e(the)p 262 2411 573 2 v 304 2437 a Fc(1)321 2449 |
---|
| 216 | y Fb(&&)c(and)g Fa(jj)f Fb(are)h(also)g(supported)e(for)i(AND)h(and)e |
---|
| 217 | (OR)h(respectively)n(.)967 2574 y Fh(2)p eop |
---|
| 218 | %%Page: 3 3 |
---|
| 219 | 3 2 bop 262 307 a Fh(variable)7 b(is)h Fg(subcir)n(cuit)p |
---|
| 220 | 606 307 13 2 v 14 w(name)p Fh(.)p Fg(var)p Fh(,)h(where)g |
---|
| 221 | Fg(subcir)n(cuit)p 1069 307 V 14 w(name)f Fh(is)g(the)f(name)i(of)e |
---|
| 222 | (the)h(subcircuit.)k(In)262 357 y(general,)d(the)f(hierarchical)g(name) |
---|
| 223 | i(of)e(a)h(variable)f(is)g(the)g(names)i(of)e(the)g(subcircuits)f |
---|
| 224 | (concatenated)262 407 y(with)i(`.')14 b(followed)8 b(by)i(its)g(name.) |
---|
| 225 | 262 547 y Fd(V)-5 b(ector)13 b(V)-5 b(ariables)262 639 |
---|
| 226 | y Fh(V)g(ector)7 b(variables)g(have)g(the)g(form)f Fg(var)o(-name)p |
---|
| 227 | Fh([i:j];)g(each)i(bit)e(can)i(be)f(written)e(as)j(either)e |
---|
| 228 | Fg(var)o(-name)p Ff(<)p Fh(i)p Ff(>)262 689 y Fh(or)j |
---|
| 229 | Fg(var)o(-name)p Fh([i].)14 b(T)m(o)d(compare)g(a)g Fg(value)f |
---|
| 230 | Fh(to)g(a)h Fg(vector)g(variable)p Fh(,)f(the)g(following)e(can)j(be)f |
---|
| 231 | (used.)262 772 y Ff(var-name[i:j])23 b(=)i(n)610 822 |
---|
| 232 | y(=)g(bxxx)610 872 y(=)g({value1,value2,...,valueN})262 |
---|
| 233 | 971 y(n:)f(integer,)g(bxxx:)h(binary)f(string,)g(valueN:)h(either)f(n)h |
---|
| 234 | (or)g(bxxx)262 1054 y Fh(For)7 b(instance,)i(counter[3:0])d(=)j(10,)f |
---|
| 235 | (counter[3:0])e(=)j(b1010,)e(counter[3:0])f(=)j Fi(f)p |
---|
| 236 | Fh(1,2,10)p Fi(g)e Fh(are)i(valid)262 1104 y(formulae.)17 |
---|
| 237 | b(For)11 b(variables)h(of)f(enumerated)h(types,)g(one)g(can)g(write)f |
---|
| 238 | Fg(var)o(-name)g Fh(=)h Fi(f)p Fh(RED,)g(YEL-)262 1154 |
---|
| 239 | y(LOW)l(,)f(BLUE)p Fi(g)g Fh(without)d(vector)i(indices.)k |
---|
| 240 | Fg(var)o(-name)p Fh([i:j])9 b(=)i Fi(f)p Fh(value1,value2,...,valueN)p |
---|
| 241 | Fi(g)h Fh(rep-)262 1204 y(resents)7 b(set)g(membership;)h(that)e(is,)i |
---|
| 242 | (it)e(is)g(equivalent)g(to)g(\()p Fg(var)o(-name)p Fh([i:j])f(=)j |
---|
| 243 | (value1\))e Fi(_)h Fh(\()p Fg(var)o(-name)p Fh([i:j])262 |
---|
| 244 | 1254 y(=)j(value2\))g Fi(_)g Fh(...)15 b Fi(_)10 b Fh(\()p |
---|
| 245 | Fg(var)o(-name)p Fh([i:j])f(=)i(valueN\).)262 1393 y |
---|
| 246 | Fd(Macr)o(o)j(De\256nition)262 1486 y Fh(Macros)d(can)h(be)f(de\256ned) |
---|
| 247 | h(and)f(used)g(in)g(CTL)g(formulae)h(for)e(valid)g(sub-formulae.)16 |
---|
| 248 | b(Y)l(ou)11 b(cannot)262 1536 y(use)e(a)g(macro)h(such)f(as)h(\272)p |
---|
| 249 | Ff(\\)p Fh(de\256ne)g(MSB)f(7\272)g(since)g(\2727\272)h(is)f(not)f(a)h |
---|
| 250 | (valid)g(CTL)g(formula.)k(The)d(macro)262 1586 y(de\256nition)e(must)i |
---|
| 251 | (precede)i(its)d(use.)262 1669 y Ff({\\DEFINE)24 b(|)g(\\Define)h(|)g |
---|
| 252 | (\\define})f(MACRO)g(formula)262 1752 y Fh(For)10 b(instance,)262 |
---|
| 253 | 1835 y Ff(\\define)24 b(Red)g(t_sig)h(=)g(RED)262 1884 |
---|
| 254 | y(\\define)f(Blue)g(t_sig)h(=)g(BLUE)262 1967 y Fh(de\256nes)11 |
---|
| 255 | b Ff(\\Red)f Fh(as)h(a)g(shorthand)e(for)h Ff(t_sig)24 |
---|
| 256 | b(=)h(RED)p Fh(.)11 b(Similarly)e(for)g Ff(\\Blue)p Fh(.)14 |
---|
| 257 | b(One)d(can)g(then)262 2017 y(write:)262 2100 y Ff(AG)24 |
---|
| 258 | b(\()h(\\Red)g(->)f(AX)h(\()g(\\Blue)f(\))h(\);)967 2574 |
---|
| 259 | y Fh(3)p eop |
---|
| 260 | %%Trailer |
---|
| 261 | end |
---|
| 262 | userdict /end-hook known{end-hook}if |
---|
| 263 | %%EOF |
---|