ÿØÿà JFIF 

  
 
  ÿÛ „ 
 !.%+&8&+/1555$;@;4?.451
4,$,44444444444414444444444444444444444444444444444444ÿÀ  á á
" 

ÿÄ   



           
 ÿÄ ? 
    
 !1AQaq"2‘¡±ÁðBRbrÑá#‚’¢²3S CñÿÄ 
 

             
ÿÄ ! 
 
 
       
!1QAa‘2ÿÚ 
  ? 5˜Z¯V¦cø)›t/? z¨±>Õ5€¶‹Á¤·¼z¼Ü¬+ñ®v¤¨_ˆR­BFn©—˜ý®ç̝P8gýt·ÉSTŦˆìät?þé¼íìN/Þa)ì–í6ô…
Ï¿øÃj´¿KÇü]ÿ ªô¹-eKànëÕHTx}ýSÜ›ÿ ”7Ø×&µ<¦  ¥ÑO¶[Ù¯ä¨ÞÃÿ PZ-¬;#õ|•
oaÿ ©CìÞz3˜öː/¤­ñTûIØ}š^   mÓ%ªxˆ¥ÉŸu=Z+ISe¿45™¼u;ú&WØ÷€æßQ™®{|
íx*TC“#ZŠìZ§²‹ 6pv…³¿¡äª*áZÐ%ÒOáˆo"x«OHk
w±æ+¬V(kMúŸ5Vö«$ ÁrÏbàb57/luR ¸ÑÛj Òµì`Ðœq­û žICÀ
Ê•©4€Âcà¨Ï€O´<èÐ:›ù(Ë^L8þ‘ÍÌ#¸Ð_Ì©ÙK(Öz 4¬û+¸;ü’V’84‘¬ÃŽ:[â‡ÔÌáõp¢~§ªlæ£ö{®G>J¼"°‡7¯ÆÉèßû ‹É‹§ÁòÃýâßî
^ƾÙõ‹×óH#«LP½ïX=xÑÍ$|W?•~•îëÔ©ª‹
{ÝT…Kÿ ”hûâá)J*ö˜–ÔU;iÇ€/ ÆþjóZ\ýwØ=Ìm
ºèËL9 ýè
Æð/¨’¥öo=nË.%Îì   ŽÕ¯È|{Oj²ƒE6e/ßdÄõ²Ìâ1O®ò×TsəԸhOMýíMˆ¿¼H˜l²,7Â¥#MF/Úf°Ö½± ¸–dr‹NýÊ íjqx{œÉ ä-È    ¦
øÄër¨q°ð
†nцýÑÄÆ’mä…n<0È™;ÁÝá¯ÁZƒ7FÀmì­ É&9ˆîéi¶ùN§Y•ÃZãAâ?•‡©‰ , ó¾IŸŠc1 4â&y­&pŠ­6;M À 0¹qç»p.á …ŸÅáK@<u %Ü6ÓtIÌpÓr»söfeÁ0O…­´Kƒ&ñ™\©<+,~)‹
ºHÐ*×µ&†ž‘Æ÷ÚŸ
1ßjC5Oh´‡›

Ø×ë æâ“Þà

ÒT]§n{ºöB³ ¦ ̹Â8Êï¦MÉ<„¨s¹¶ì7Ì”æR$Ncà! /éþäRM÷Gƒ¿É$
¦oà>%6·y6ƒ‰3?”úºŽ‰éX5ªPT §µ!=Mž«Ú½‹ÅgÂSâÉaþÓoö–¯ÁÔìR>5éÿ üs¶ÆUcÌ  kÇR
]ÿ ù¬¼«VŽ;Â|‡~¢¦”ÏÅ°æ
{L™Õ°Óv¹ò¸írŽ¡×¢CÃ!íVÕ {¶»sŒNPg/
"uÕbkm²“$ďå¿é¹§°½æz¯6 †s¿!s–wÚÝ“™Œ°.ûj>·+™Òa…©Œ&rÝÎtÛë긪Ît’LAVp%c Úý[ÄzJ¾ÇàXXç@˜ó<êL]·T˜¾¥1Ó©V‡g´æ½¦Ý@¹óø!_@´ÞâSÁ —S3™•& ]@JHÚý©ZŽ €×æÔr»Áf!‡yÞ4Mv*èÓã_{‘åóUuљØ«Oïé*®EvÑ
Œ÷‡U \"㪒ÍK+À 4“M¡ï:0¥5í!'<@î´”>Ç»&Z–ïCCV˜Ì5Šo&îhè.žû
|ÓK©h$s6KìŒëã)¹hI¦GïOåóI;ììü#É$Š0…Ææ¥TØ.5­¾gn´ “ÂÖ\:hœ89G)J@„}œ:’Ò{/Š"¦_Æ×7Æ3VÇŠÊa]ÚŒÙ€Ä–=®uÁßâACZƒ§§£Qnâ:«,×{tyø¬iÛcœÜÄ€H½ÄÍCk´÷šß
.W'b¤Íåh]÷€=,Žv×cÚEÚHXJX¶îo¨FÒtèöŸ>ªª6[J®Fµ£sGÁeqõfe\íjÒÐïÄÐGˆe1Ø‹.Ø”‘Ëuø
Y­ˆÜŽG|zùªüMpDnQWÄ”%JŠ™)â*p@Örš«ÕT2Ð%ˆG#ª„
·¤!°ŸOTÂT¸aÚ%4&h™LµšØüÐ.F¿²ÐÞ_Ç‚¾ÅÃaÜ÷09Æ 
q€öy˜v‡85õN÷]¬äѼóS{°_MŽ¬úÔ#°Ç¸0åÞè2ëôPcvÆw9®ií1Ä8F™˜à‰´+‰Ik1òÝ7“Ñ×ÒsÝ\x‚h`ÞÑ`ó"|µEcý£n˜h`}GÞ  !±ù²Ápü²
ß6
0ïi󜵩SÈÇ7˜-ÕURO˜¦´f$ªž-Í6(œ}<„ éc øs]ŽŽ„*—¾
ìdŽ„)méª\¿êÎIg¾ØÞ~I#C/¼¼´EÁÈŽi8“©õådô·>euä ƒ'Ê×लR1ÉJE1ÐAát`t;ÇР%Ý<‡¥„ÍÆ`×Oyó)õiI€ñQaŸ4Ûù\áàaÃÔ¹HÃu¹*k€¦<„eS‡&õÏ
B!ŽhüÞ`yj}mªf×\¿
Ç~æ­9‡û\՞Ǖg²1Žû5V7 !àöšm°
c`ܬøÇìµÒ'P"?…´Ö,"§^•õŽ¨sÔ)6˜sæéÍR¼
ò|Sl”‹7 nPW

Gòú÷½§O¯‡„l¡kSÞŒr½PÊ@æ¢pŽ-mÿ #Ÿ˜Àº¶Áä¦;ïÔæ$1££`“Õ>„—·ž)ß
ð
³ñ#Ï Ô$¶œ‰ÊE‹À;÷º
¯«P:Ñ”8–IÊtpÞ3ª“>ê“þës4ò2OÏÕ­±zô†Õ§‰.÷ä¸;¿˜“'œ›žª}«Œ{ª±Ì 9ÔóÞÕ‡0
$íWV3Üì¬
—@kÝ4@¿r¼±½¬™›?øØæ´'Áé®CË3-g$˜ö‡×auÚi´Žp/êÛæF›Ú2v‹ã¿¿,nB1̨ƃqÞa5͝@&Æû“él÷ \C²½UÍc ¯k×¢U
ÖéQå™—-r    wô ÞÏ<Ò=&=ÿ Ôê Òêˈt,i—;LîÜ á¸*ÚÃ1$êL•LÍ <É)ýÐà’
;F™{ƒ™˜€&'}‚ãÄK`¡ÞT@I;®žZóè‚s’7®°›+§O­Åq©é»²9<Ô
J ¼9O’HL»Ùïì¸rk¼Ž_ý‘TŸu[²ßÚŒ·ü÷B%¯E ŸÔX5êO´Ç•€’I0 É<mÆÈJoúáõóQâØòÙaÙt:  ·=|Ôaz]a1cÉŸ1
4˜à3΍}GFøí7/B«vεŕL=Ðr1ÕšnwH›óÞ¢ºö{)´4€æZç^ÿ yÑ:_([¿ipqQÊ^âÆe;»½“¦º|¢ÀTçèrú1”óTÃ’u¦CG¤ ¡
Š­7ë

·i“¿z»n
ö¼±ù^ö<‹çu7¸ÈlvZðÛAUXje•
dLÞH ÚosÇr`È™‡pÊeÇ4@x7´)ö†Ótœ~i‘Ï[x@äUÃæ­m·e´x
°t¸·²5'žªža   =ÖÌåzϘ'-´ˆpž3§ò‡k  Ý'‰ýÑï¦3ºdè“{eiÔõNkîšECEΠ¥ÃT9ãqÃâŸîɐ8z \?€    >JX` 
ñ¹õ%;µŸD‘«´€àwÒ™UûئžÖö\×®×´8 ½‡ºÐÆÓ§?Àkmœ=;d5*@-ì0F Rªýš[Ü6âö̃ڸr*KA9· u*µæ£?U¸Âêí†8@¦X4 e-ò„0s{ HâUpU?¼mñRa°®a%Ð'tÉ×’\¾ÊÉ]t›h>·(Ë@R¼¡Ãt h}’O÷au<+nT…Ö…MӐ??Óe95 q>í/;&JSû °¯ÊéÞøƒ*Ã2½Ài&:nôUl=¾¿5eˆ3”ñc|Ú2V”>„»&eE;«ÚäC
p¢Ûúy 9š[ŒÌx¼擼A&DåÒ¯ˆ¤ÀÌ;"˜ÏQä¸åhÊ}Ûq«Û0WžÒ|»€ø®öCm5•\ÇÀ§Pe3£]0ÃàLDÉ‰1øªxjgwT‚÷¿LΨK‹›ùs—xˆÜ±µ
kæ¸f‰‰ÜGk/LÛØ6d9ò¶ùA{ƒA3š/¬D¬khÓk‰`˜"㯒r¿±Óã jx‡°e}<Ñø\3y:'À•/h½Í€Ç4~g ?Û(¼]v‘ªlKÎâ~?O‚W%{Ì:“'©úNq¾›úo(X’¥¯ˆ
nFê{Ç€ü?º'ë
ø‹ì
Þ09ŒÌç9Æ —ËC`j@ÓÄ(+a‹un¸#ÂꟋ{K`‘ÑÍÍ'à´»/Û,KW;Þ4²þð ï Nm|~fGÏ(…³Ã)«1ö­Õ
¥‡¨©ƒÃ™ü-s=à=U66Ï«Ýc蓦W¹íž®›nÔ%êÇìŒ<#Ü×84ån®Ð ÒåOC`  ñânÑs‡¢ç 1õ%Îhì½Ã½® e:ݼUZo
™`  
ÅZŸŒÊ«ê1ÏÄo$q¹Þ€©ˆhÐÉä¯ñ[!…Ú˜àJ:x2$Íß&PåT£6ç—
‡Í*4Ýšçjÿ ‰É nófÐ ó(L5C•åÆ\rMÒ@ò
}y-W}™üýVù—ú¢=Ù”c®‘< M ž
´Phr¦©TD ‘ù.$´÷O‡‘V2Æò.=IUŒ=ž‡â¬i™aþÓåÙ?òUø'ØÖ•.~* šTŒ!•-×áºTâ®ä#õü'´ eýlYÅÓeÕKÂrT"CÚ@u!Óxƒ{š3€}1¿(r}%«nËamjÑ%ÑNEò
v  ˜à  σöK³,*º.àzù¨™Ó ÚçâU¦*¿ 9{%Ö¹ njûdaXöb)  kÛƱûÓ\°M7ˆÂ=û›ç¿Ã‚­V»Cg–8ÙêE-j)k$º`Ã-ùEýeBÆÇ]c¡°ñty&Òd0nõ'¡W+ƒ*|–ø<K\%¦cÏÄ#N,Úú‘¤òÒÛõ ’¶§‰Ì
ú•dçb31Ð\7‡ëÚw82
‰KÝkÚñ'¢Ž…[&¼ÌAÔzHàP *اoßreÁY¥Ñ¾ãE|&QbKg]ã„þê*b;R³Öi‹  ±î$£ÈTm¶k÷ˆ
¦»Ù¹i¦¨6 h%Á'Ú
J   \F±â+‹b/Å9ñå5Àë­nˆRv«¯#„&î„$º’@:‘Ôrø+,àq‘秬*Úg´>µFa\GQªEAÔp5\Ǽ·¼Ç8·õ -â§Ú[
‡
uZeÖ 3}×d'+¹:ð+K†Û®s!Ï$úe€<Û”x)1»a­¡LC]¸µík…ÚàA»AYº{†ªS[¦5HÒ7ù
--,ísòDØ€èk   ÞÀîÜò@â(  ËNˆë›4ô½•/¦o‡€Û7
ê•ÆêòðÜy
'Án½µ á˜ݦ  ndeo…[ì¶Ê,¥R³Ä=À±—–ß;£™´ñSâ*g§”ïaið‘Jå~™ÓÞß³Õ¢»8x埒²52>AÊb&-÷\7´éÄù€T˜,w;3{ï˜k…à¹ÄqÀ«œ{
€\
ˆ¾[´¨јr &Úé„Ívˆ±8†¿]|¬ņ4I×pÞS1ÈÖz‰#Ìv‡G!YNògñ:màTz¢Ý1ô©^O=~ë|5Bã™ç•¼µõ•bÆ@úÕS¬ÈŒ#¬zünrŸ
û”
Z²•ï›èðV"ÁHÚý©wÝ €7¼Ìu1hÑa3Éä û f$o¿É ™Ú›ÝçnpÒ3äÌ3†Í§,Äï]$‰/pê†«À¼
¸e9­Æê_C]žƒ·ý·frÁN«,E=›Çq
-‰öŒ:aÏ¿±í&£Í:-}
84‘ÿ eƒQÑeëSsuiA
³g㟥ú£?ÿ ʼn*”“÷aühe:ÊWa@ÒÞk±eØ]
F Ô—r.åä˜@ö¥ªZoÐýYL·¥S²G/‡ñ
<~*ZÆ´è>JlòàÛƽÿ 窘ìGN¢:I®KšJp/`íIÁÀõ#Ä-€ö­šµŒoF4|ÆQØÆ@Ì|£Ô…¢À{9˜è½Üó›€ôYÒÎYsið;ís¤€à²ˆ‚4qÉVŒI$  ‰"°   æµ8cXGjœˏ¡Aâý•ËÜ¢ûïe·çLx']á"oÅÎê3¯Ç—¹”ó0nå‚âg{Œñ>
S´˜îè°g238‚ãköÝfÚd´6Ò€;ò÷±¢™¼›º¢Æ'¥Ðx'e¬ç
]bÈÆV¢ó‹kýBO
ðÊâ$Ÿ!×T
3Mýמ
žìٍàÌü‘8÷€àæØ8æ©6‰©L´«…oãpð„~Çk‰!ñ;‹”ÛžÍ àž±z Ÿôû øŸÝužÏ;ÿ #|u6™Þ¬ÚˆÐõA4¶â|ôl|Ê2ŽÇ¤ÝÅÇY.<#Aí.k§hóF‚”Y;
M½Ö4hŸ4&›­¿tès´%FìL¥£Ãk‰ÇT¤haÁ¤ÚxfÉ`ÑìË›>i 3t‚:,–+^÷´–{Û–Nxi"x‘Ûg
î¨>¥Õ܁ùZH,2Û“:8xÊ¢Çí9.É-Ìâã-=çjwµS˜dütžçwýGòú®®ûº_ˆýx$–¡ãøO
EÚÛÏ÷R„×w+3£Á£öUMyR²¹âŒ°š›¸Ñãò9§Ó_Dl+Ùßc›úšGÅÌc†Ž!Ko=¶.‘Îÿ c²(2®V mª.ÿ ¹B›¹å ù„öŸSV>™ü¯$y:G¢Z×àøúdî¹û­·ýÇ´:•c LÍõi_‹ö+ÎæGÊè>OŠ•äž´§Þ{X}¨1ÚTc›»Qþ•êô°t¿OP?eæ~É{5]•ÙR£r5†nZ\ã@
&îJõ ¾àC°þV>fé¥/ü5ñÊIº_é5;e­h<@
Ä&æÃëE%;X,ÒãÆÞ`Oò¦kŸm#˜!ÀyÄ¢|
óLšò¥Ä`
¶R=|ÈCâh5ò3DˆïF†ðÒ#ÅìÛœ?¸yhBãœí
ZxßÎÄhºRK„`Þödvײ™ÀÈÑÒgŒuYw³%†ƒÓzõ ÖÏp‚dH®¦A´ù§»ÓÇMæ~)ˆð‡û:ù&Ä •vGD´À 
n
Ý
‡¼Ö8Fö   óáà£~Ë¥x`oK|Ä?fxiØü%pìR>éò+Û±éÎ>núlFŤ'tq8LZÏvÃ?„¡ß±È⽆¯³íü@x|PöUäèØã¡ð‚ŒAìÏ"vÍwóŸÍ{ ý0.z    È•Ö{,N¡£¡ŸKÕÙž>Ýœþ ÍÀ<n^Àïe€Þgn¹”ÜiQê
9Ú±‡„è]ËA¿‚MJìiÓxŒn-ÄS6!ÓæÑû*jÎWøìšÇ뙦gj~+?\,Ö7ÁÕÊ”G™q6TF)óCç<ÓšÂUé†gW=àà“hóR³ÊQì<!÷ÇpR1¯u„De,è­vvâDß~žHå‰ú£Kìní¢ÐçÅÄÅ¥Ü÷
±ÃìÇžûƒz\þÞ¨-•‹
€

¸+¶n¿^
?†[ÖWóÒX¸,0Ø:l?‰Âý«ÿ ·Dc+fÔ[ƒ›ûªšx«kæž1KI…<#'nž¶\±íÎ8¤ìK@’@J¥v)º[Ž±Æå´¼
½Ý¡ç¯ÐO¥ø®è•Óȱ߿wša©“œt‡4îyªœ&+1ÏØ:‚æƒ=/ꎔ`hm
“=©‹]°g}ì€DgUƒ8¤qCˆãáÅ,‡Ô¬ñ10HÑDÂbáÂÿ Œ»v·:uòB6»áp‰>°<×EA!Å‚D™IúOÍ
¡>ôG}Â`ÍßkÜL™Ž  Þð™
{IøF²
¹òQ3&!ÃÂÞz.d&Ï-sH¸,Ôõ˜ŽP€
77ˆÝ¼ÊëÜw   =cÕ
Ú,ØÐ5ÎYÐ)ì´öœgŒ[¤
ßv㙑8心>h]§µháYš£²ºÑ.{Ï7Sð•?´~×SÃKýJÛ˜
™Íäiúu<µX¶1õ^kâçIÑ£sZ4h>j*ÔšD:4­¿_ ÷¸
Õxæÿ ¸?Mù _•­ÊÐ ä ÷ý ÑwL
œ­ïnTkÛUÍN©ë:¦fV ¶ÜÔÜMªÅâA½–¿R×TXš-%iTÊT•‡Ù‚JôϐZxWÑè‰f‰òG º
×Õû2aZ7OU3[“×AT–ÞŒ…-‘¤”Ì 
ì&(ˆ¿­•ƒkï’:ðY¦W‘Å)“†‘˜³Åtcø˜ñTÂwÚÇ4
|üLÇªí–v-
qˆèU
qPE.†â‘˜µ Æ,ÐÅs]8¾„oúÑ i>ÜxxÈó)ƒ ´æÁâØ$À‰vžŸf$Ž|ãw;ÀÁIJ»b`
{¦Ó¤Ú$©YÀ‘n@Óïž«9J¼êG   m¤
ܯ¹ÌW4€ÐÒÅÛ‡#褕Ÿn-?í|с¥÷Ú¹¬'´ÞÜ9ÓK`hê£SÄSà?7—Wí_´…óB›»:=Ãïq`<8ñÓŒÑlú2d¬ê³£hÖ[l|$vÝro~'R®‰§°ñmY ͧäP
|PUª¹·:3Œ[Û{Xÿ ºâ@‚W–Äé u‚ ¯´*=íή.pûÒdt @
G‰¬ s¸    ëÉücr ÞæѨÊ@>¤¢Ö±.Þ'¯°ÌME[YéïĵÂCå½
Ué©Áû'Ê9%eÔðNU”ë‘ÌsD3/®+UI˜9h.WC”
빓$#:pz:YÓ ¿xž* ³$Í +$kñAŠ‹†¢
Uê>¸)_š¬÷©ßAÂÔb9ÇU ¯¾
á•9¯ÏÏ÷O÷¼¼Fähal1‰3Ì[Ïr•´UCksNÐ]R‘¸¥H+§Šé†c©vÖÞ0iÓ76s†î!§=ß
¼~Ô'°Ãmäoäš³ªøi1úÉ)³yV8CLÄØÁ‘WYïi€H6ÖÑiámø^ÈY´°Ñ7¥Û*—Ñ©L«Qƒï—Ùrÿ ›£Ð*š¸ˆL©ˆ$ˆ ÷¾D§9È®«qbqC)–ˆïv´çñsÑVT­Ø, <àïºÀO«Jý·õ 
àfPìð  .wFšir´þ’2_Y
*Æ€x\«
ì€9š@ Ž|F⇥ˆkZ@hÖÄ0t¿-<“‹qµ¾*ZL¤Ú)&BJpÓF5=$„at*Zš$’ÑtdûÝRI1    2Ž‰$€$I$#‰SÞ’H
ë¬ï;Á$¡t$’`<(ñÇt)$‡Ð.Êf¢X’Kt=Éé$‚ˆªè¢oÝëòI%Rgcª÷ŠyI%¡‰ÿ !ñ)´õ $¤ Ô’IIGÿÙ" Vim syntax file
" Language: Murphi model checking language
" Maintainer: Matthew Fernandez <matthew.fernandez@gmail.com>
" Last Change: 2019 Aug 27
" Version: 2
" Remark: Originally authored by Diego Ongaro <ongaro@cs.stanford.edu> 

if version < 600
  syntax clear
elseif exists("b:current_syntax")
  finish
endif

" Keywords are case insensitive.
" Keep these in alphabetical order.
syntax case ignore
syn keyword murphiKeyword       alias
syn keyword murphiStructure     array
syn keyword murphiKeyword       assert
syn keyword murphiKeyword       begin
syn keyword murphiType          boolean
syn keyword murphiKeyword       by
syn keyword murphiLabel         case
syn keyword murphiKeyword       clear
syn keyword murphiLabel         const
syn keyword murphiRepeat        do
syn keyword murphiConditional   else
syn keyword murphiConditional   elsif
syn keyword murphiKeyword       end
syn keyword murphiKeyword       endalias
syn keyword murphiRepeat        endexists
syn keyword murphiRepeat        endfor
syn keyword murphiRepeat        endforall
syn keyword murphiKeyword       endfunction
syn keyword murphiConditional   endif
syn keyword murphiKeyword       endprocedure
syn keyword murphiStructure     endrecord
syn keyword murphiKeyword       endrule
syn keyword murphiKeyword       endruleset
syn keyword murphiKeyword       endstartstate
syn keyword murphiConditional   endswitch
syn keyword murphiRepeat        endwhile
syn keyword murphiStructure     enum
syn keyword murphiKeyword       error
syn keyword murphiRepeat        exists
syn keyword murphiBoolean       false
syn keyword murphiRepeat        for
syn keyword murphiRepeat        forall
syn keyword murphiKeyword       function
syn keyword murphiConditional   if
syn keyword murphiKeyword       in
syn keyword murphiKeyword       interleaved
syn keyword murphiLabel         invariant
syn keyword murphiFunction      ismember
syn keyword murphiFunction      isundefined
syn keyword murphiKeyword       log
syn keyword murphiStructure     of
syn keyword murphiType          multiset
syn keyword murphiFunction      multisetadd
syn keyword murphiFunction      multisetcount
syn keyword murphiFunction      multisetremove
syn keyword murphiFunction      multisetremovepred
syn keyword murphiKeyword       procedure
syn keyword murphiKeyword       program
syn keyword murphiKeyword       put
syn keyword murphiStructure     record
syn keyword murphiKeyword       return
syn keyword murphiLabel         rule
syn keyword murphiLabel         ruleset
syn keyword murphiType          scalarset
syn keyword murphiLabel         startstate
syn keyword murphiConditional   switch
syn keyword murphiConditional   then
syn keyword murphiRepeat        to
syn keyword murphiKeyword       traceuntil
syn keyword murphiBoolean       true
syn keyword murphiLabel         type
syn keyword murphiKeyword       undefine
syn keyword murphiStructure     union
syn keyword murphiLabel         var
syn keyword murphiRepeat        while

syn keyword murphiTodo contained todo xxx fixme
syntax case match

" Integers.
syn match murphiNumber "\<\d\+\>"

" Operators and special characters.
syn match murphiOperator "[\+\-\*\/%&|=!<>:\?]\|\."
syn match murphiDelimiter "\(:=\@!\|[;,]\)"
syn match murphiSpecial "[()\[\]]"

" Double equal sign is a common error: use one equal sign for equality testing.
syn match murphiError "==[^>]"he=e-1
" Double && and || are errors.
syn match murphiError "&&\|||"

" Strings. This is defined so late so that it overrides previous matches.
syn region murphiString start=+"+ end=+"+

" Comments. This is defined so late so that it overrides previous matches.
syn region murphiComment start="--" end="$" contains=murphiTodo
syn region murphiComment start="/\*" end="\*/" contains=murphiTodo

" Link the rules to some groups.
hi def link murphiComment        Comment
hi def link murphiString         String
hi def link murphiNumber         Number
hi def link murphiBoolean        Boolean
hi def link murphiIdentifier     Identifier
hi def link murphiFunction       Function
hi def link murphiStatement      Statement
hi def link murphiConditional    Conditional
hi def link murphiRepeat         Repeat
hi def link murphiLabel          Label
hi def link murphiOperator       Operator
hi def link murphiKeyword        Keyword
hi def link murphiType           Type
hi def link murphiStructure      Structure
hi def link murphiSpecial        Special
hi def link murphiDelimiter      Delimiter
hi def link murphiError          Error
hi def link murphiTodo           Todo

let b:current_syntax = "murphi"