From 686f353bed78610242a58f742a81ff09ccb964eb Mon Sep 17 00:00:00 2001 From: Francisco Penedo Date: Tue, 9 Feb 2021 17:43:57 +0100 Subject: [PATCH] Added templogic project --- config/_default/params.toml | 2 +- content/project/templogic/featured.png | Bin 0 -> 28853 bytes content/project/templogic/index.md | 236 +++++++++++++++++++++++++ content/publication/cdc2018/index.md | 1 + content/publication/hscc16/index.md | 2 +- 5 files changed, 239 insertions(+), 2 deletions(-) create mode 100644 content/project/templogic/featured.png create mode 100644 content/project/templogic/index.md diff --git a/config/_default/params.toml b/config/_default/params.toml index 39a26d5..38009c8 100644 --- a/config/_default/params.toml +++ b/config/_default/params.toml @@ -57,7 +57,7 @@ description = "" # Enable source code highlighting? true/false # Documentation: https://wowchemy.com/docs/writing-markdown-latex/#highlighting-options highlight = true -highlight_languages = ["r"] # Add support for highlighting additional languages +highlight_languages = ["r", "python"] # Add support for highlighting additional languages # highlight_style = "github" # For supported styles, see https://cdnjs.com/libraries/highlight.js/ # Enable LaTeX math rendering? true/false diff --git a/content/project/templogic/featured.png b/content/project/templogic/featured.png new file mode 100644 index 0000000000000000000000000000000000000000..bbfca4a2bd60127402658e432d2eed5c984e330d GIT binary patch literal 28853 zcmb@u1yGg!*DkyfF-VaR2|+ZNAo)H{tm?!OvC^7|MimYbZlWA50CSKG_he5 zJ{}%Uv;OaGZCR303=v4QC}v8^zb!!z-o1M_oU8Jgj}VL7YCK(@jz%`Y%<%m$Rkzdq zmFaqS9UYz9m_!tI17e}1uG_OO`jQ0TCBj1d(_yJMajxyt?>x04i{FKcZK>1=p&F&H zB_zJ8<|rB;u8*y(tSGi++dFMdPt`hajaOLI*4E+>J=JduB~uhr=B}=;UR+#^j*dP# zIWaz+ZSXw1g-xoSr^;+$v37c})|bFr7C|{L;Bg%0zdDqoG=>(n*&WMaU|`^fLmthI z89MjPYC;q_*BXLXTI|$ZsMjcnJJsN+#c07H8xRnnlqG95R+^ERsFSB!Ab7f*Hb4J5 z=Y!%io9XA2n#KC>zAxC@+s80z4CW}&iix%PVv&TB^6vilh!I6>ps}JoP4?X7DJ~is z8ufo(G&HS0f07D%@bK`Aj*LY6YgU-6jHH#Jbai*HPuKI~R##P(TTP6#w)!Tfd7Q3f zDf+42g7u+Fg+ZcUwSTycGwrsz@2{`?SafQXb;G)g8ZRZ0unkc< z@+;>T7XfB}e+CTtHrY;!k$WPMYrl&glok^<%gV?^b-c#L#wO5<8W^v4uPi7ih>abK zw`tI*wAOK2&eo}Ql9mo0`dXhU_URGQVZI&rF-F_ZpDyn1c;TNu$(5P(ba!|Aw|91$ zA8k%Wk!8K*i*dFX&J{trAFk7%j?}v!X=`iyFT)M#*Uath>^7(C<0B$cLx>zjyu7?( zSae9q$Z*K`elFtU<9nR%w5=cEk&!W5x%?q6*VFPNkCpw+Gn70T#2SR9>h9@5MMdRcXCF=Iieas-uErfGHfT-{kx?-)_*!2t zfGgmAsXg~&XJ_Zpqene)T(ypCgzmB{DlZ?-vE9f4HAhD}1^ zKYGOS`p-ZA+;nz!W@OBR(WogtH);!|PBmQ192GgNwqIh%F}sL}kGB9@wX)KYmj~~` zAY`IQJ=t5bu=tqavEoZBATZU^V!S=uWWG0MJNV-VB|pDb#P`4&7&h*3o|;_y4*~bX ze5EXGZ$T&M689oq~lcPwfnK3*eOz+#OsWWmYCJ8CQ@+{6 zw}Nk~>Vq-XVc3tJtINw5+s=troaodzJf>8&c_O0Sa?k6nxVSiv+rF8)`WMX!X*oGL z)xCUvKjf5opZ00;F-#%;nT^xix3hVQ!;{taS?0sJ`MK%KrZUpfftlIp3>nDGl$2SR zOoheokx^;2ukvq6)iURPM^H=MxN#$}x39OCCN)gob7(DBhlEG;daoWAAdfuwZuUtkpM}CRjoBaaFQ|P^PPVbO)?L?<*45SZ@Tkkl zc{5ex7{t=*RZQ?ak$EPmW4F+Jz^=M(KUvPi#KgnH%dJ#lWzbs;P*IiUOo=Y-}7i zG>%G6-kP6BBE!SO&qWVbeu*8ZPo}*1U^VgWjW+oB9|#X_hwB~QBZGsxYekJLOiao; zumRn@z1BN_TL95WguFb!@dMhMnhZ9^D@1;~!tXCH&L+mjRB{wEWa7F1{P}Ymo0K9| zx8CjU7@ukn3GVf)NiXh8T--GjJC*=Irle4e-1}tf;4m~gvVOMJ2=h0kH4P07J)gF_ zJa_$us1^LeZY=ro<&Wiov@wIcbmrkI)JUY!HsI^-(UDr-8UQt5Ms7?@j5N*O&d$jn zKk{gZGxhGyHa0f)_InV%>`0xDHg)*5^`1eZBh`)olIIv^%ogeo6N6gbL@n-Bzrvtu0cyNVk5eFWLLz;CF#$MQKF^ z{JjbRCU9fx?eX@X#h&;w`v+1|T`(&zcd3)X8TTy#Z||$)W0zr-l2=U$y!JzZU!K_{ zH8u))lhS1%A1l}zpOluHo$N0B@D9cy7fj%HW;v_p=!t*UXulLXZukSo0mAj;$B$t> zx!BlpbZQU(xr_Hm$ZN9HSZX*;gIBxS?xX+u`nsLHeOLYcjlr*VfTZdGFqCnEo^J48 zb@fq*?xw&aJdU?l0qY7hx#;M!mkSQ|mim6@sz5}w1Xu!GB^Pijm!`>6$s@EN$0a0O z+}hGB(iNcG-QJ${R)(EC-tA%ypyT9JcC<2T4K^^1%st9OM@I+O$uB6t!^7i>ZnqpS z?-(Di5e*^!l_jV5&GKR1F&WQWipKAN|6}jcv?{F~SBD-xv)2Ays55pj11ra{YYMTA zJRln&eSHBO!OGGyAu+M>bT!Z4-#>~`EtHIZWMo8D997xLG{bhT6>dBOp{R1kt4o$> z_>^8IfhXKw^wXn_+1dUw(>{eX(URoUfPjvJwcjc+=U@z@67@wzTgN+d5Ti`2t$PUx z?b1T0vPvo{$k<=|$He>&e#jBctkoLV9v2svB;X#+9G#S;+vw$qff1CFlCr(M4Y!g@ z7OYn-&}{a@VfDOdYHGT?yzK4mwah!I|7c_Nou$+dn{0J+Q};C5d=f>H@`=lcj!Fd< z($X@&tgNiQ{(?5ygWY*k+i7^T&UFuNssXVik?#PeOWO9)&ks)lwx_)hpX za>0+>OCHOp*%u2r1aJ&7&U&o$F|>`df$R?nOL@#AF(HF`iGV^>TDvxbJoI>rScz&}jnL_}r=25gq2#lWE4 z0D&Q7zBZN3U0MJuy?giWdg?czx&Za${7#kt2|C)^KqCOQ86w!lf{9-6jZBO9?OIDq zV@9ROCh~co?}!bIn8AfC|GvN^=1jc~hSiYiZjbrBFFhCrhYbL;k^8WTyY_}gMlv!o z?nj$4NC=^Smdf%H`UKCU^#gz?8_+ty0vg!^`UCT|HZ=UvH&$kfGf@uKurtvji?;f^ zNUyh%qD@3htjy>-8jU5u2x7l{L5hgvutX;$Fr`l|0*W4P%@mz7YJ%Ysyg{xmEr}ry z4-d~B4J0K4KYaM0=_~kl)(2b!oW4+}_Bi(JXvnU_cDmMQ8k7G` z78V=H+H6UkR|ctRX=#BAc|CatTp?CkHA9lXitCv%uG7YNRPx^Lf|RPlw>Q6NhN(4J zp1W*QxS#B=D8VHV^()x$j`^F2@$R?TLZG8c1+oZCA-C7`_9U>};+XYH%?6q_yXwi- z)=UV$=8h`~v&;nliB4eLx9h!Dx_c=AZ(I60+S@58D=Z-URPPE1rxMHUO%U{~2}@(v zl6G8w52%8t(CBp`d8J=sp!T-!wZN;(<2jt+Si9;36(J-NS75t4!e&gsuIqc zmyeI$k}mPt-wf8DKm+HD`FyWW=$!Q3Z9b=(u?h>d;TE1yjJtOYXz3P$Ou@e)KmwQO zuh=x;8!8Osid-Hoq2fPM=5pSgq*u!P=i^7mt!V)o8sDisA;@U}r1%_HBcr1ak7m60 zFqW2<@NlyRA8i5g1j1%hx8u9Yr@^x1&LScr0_Xs#kV<}$x}xI!_(p?fUx?DazP=;b z3a`Wigf8}#AdhJer_#VMe?+q6|0&RF9UwGy{L5dk4CGL@LK^$!g1^6P(sN$@?+6>4 zE#Q!DE-uBfKz|@wjE#)}aF7VNIV1~u{=?}(hjvz0EQD(h*6{J=ABgWY22V-brW(EV z9JRh#jzvU7up9ooOLtEi_(T;+1CHaQ2BX!)!2fPo43;O7vG3z_MTJC8Ja%5nvM% zx`ObF{E7YX`8#)=fuaWKkldkbU!{-fV%2Mq79r+{kBb|D{P^+XcNODQluo}JA?)Nf zs!|#*S)F%9G&oee`Ux!ik$@W~I5Roe*fnt+8?zi8cimegAS5j9BzjDZu95j(Pc?Ra zX{iw?3;?DM*a!bGU1chNKp3iyuI@CDcz-h(ws}Zb;O52;X031Qkh@@EVgjiMa*FSI z^Nw?+foJ`acg9Hqi=Xdv=dkbUpQ7xIiORAT>zM`_By69OmVt-IbKH~T+JYaZo#Hwf zjSdWiC;zIlHKIHP);O%%VA4ZONz7*WPwUfBJ_r;++zA?WE^N41#GL;1b#MQ?U+wE| zZca;2%%xME*lBs7hwmxX9*qvs`YYQpkO{2~){b5!l_P3Z10c_DD!A~%fl+D(Fx5`h zxt5td1#ty*l!+3fHdwvUj!D?=uEs9*3xG3?Q^F{Gr|Ki=Xon!O+|R@Qqylb{b5-zC zjJwJf5+${g`&UX|y{|4R zN0XQ>*Hsx#f&&uuvNAGo2Ow8D+L~!JY(clMusD`p$-KoIlq59 zL*8rJo8StJ6L<~ag~R3f2_dtlnf3`dOufU(An-d=V`B|A9*a8<8=`~&g>y!9Q zV{B@Q!5hO${m98x?exF*9KvSjYj&rIPKV|GKcIK%0jUT7T(CQFp7E>%e}eE>LTGCK zHMb=h$kUfEW)>C`#RjjuOdvagysHYV67Io(AIPARs|+$4J$=XIWCAs}*GKd4$W*h@ zg=r3{RjcFOg)ZPEKrKse-M+dwB5$(=rfW>4k*iR^PQM~$DiKOXIZ~vToRH9+D{%4( z3Av0q8okAz$LU}XcdtqV9ru?NoT~H9$IIWC+g~Fd@OV(UHfI|34k%UpgM)(s1-7PY zV-nrQ$Hq!V6qz;4XDyO$K3bMd;CX=rKUZR;WMSC^Mg(LgzamB$@(falbwK%9wX0H8 z+j3q#={>u0hIEUP!FVF(~}xvJ~sfmAoY zgESB493n_rX(7+kNq|v_iH8KA(A4 zC=Gn&8>^Ouz%$wfi21qLX_wk_1<0+D&@}^r88uumTjbgwZyPuvMc zGlY*ufhK}pIOBPwQ$a&fBdS*DJjQD&fjaY+^clqFfByOBaARWcw{*VgJY+LcnXmG?|zP6GE!0#Rkm~BY%uCB^!tjb85tSUG(iCY^z|6t zCA917&n96--c?feCJPC@o&63en)P&@hQ9YU6%Nq>2Px8x{ zYLDfw5fKtt$Mw;Y(I913)}mMr)6LP6SM7RHSV^<%>)H-gobR+4-rl~KZMH2^)Xi-@ z3CVafuyb-=yC*a>nQ%Q=mZifZu9i(l5j7srUOH0HZKWY{>kC6a@kf(ygVLe&Zbcru5!5`3yO2#i(%pj_=&ZmBS2*0-l zr5)1nWG)NUhm{fzinLzTBlo2UwxKt+Jo*!jR0^I_^pqZ#Z-u1w6> zyCfTyyi>EAhn#J9@n`_O#44hyLqcTq_4Oe(*Vol4FJaJ!Z?xrxNb!btb#!PzdeX=c zZE}p^?5m=F*Rs0OYJwYNW1Gf{Z;{5Ssi{M!e>xU+0agGLLw>h;p6-ABJrP8RkB>>p z6Qt18O$c6N5^s!AL5?sKhJ zw{PE8Q~M3dxGiZ+e0;6fgM!4$ zR`ldDBYYv3o}X9VZ)k`sFXsfxUQYf*s<83mkVL4hwN;enbIC0%X~@W8Vjkc^PPD_J zk&&V4ofVP&Q72qr55O>AP^lvPg{CGkiJe%*2N@6)A-Ars=FJ;lfS8Ir;46(}tuHR_ z@9xfrhymQ5gv%WN3OAZp5Qt~2^x?GoR#Xo1ao3%z($2@!)ESVtf&5~8l-2dl$_ug< zWm8d6(b84pVXf*LI1ZM@p>bRmx!hAckUpH*g5Du)ByLyz9O7M5(+hnI)Q%O&Y2#N~ zm_$!!^R7UHod&|vXMG2vx=;&tXvfZ5wB=h^q7G>vHe;kZ_y2c0*&M5Brgw7ReIU%&!5PVvm|C4 zD=PtqW%&xPnso~kp#s4Ft%=G{-WILF50OJaWGaF%56#L__t2tU;L_o*zM#;v*)K|8 zN+w?P#&f<&{bn)}?(6NLLa&a^7y$0We@e>lln(-vNA~)1o!J0o$l4MQ3m>0mMWP6Z z=hqsV`EQjoma@!y=Crdg#!O1N?4G_p@~8TUnTTs$;99Ct8-@r^a37LtV3BGTbOVs^ zc>QxPbPh5L$TrP}zZ!!Q0zo>%?Laj!I2hB*V-^_JH4c#vzc`Mzi*ve8u>^&LW;#11 z4_ehB4Uu}&qFArix%zV0TuI$33(5zp-P_x5y^`6uxHkH~HiJ4S8{ImYs8f&}bl?zL zSy=E}jdPBqf1jAp5`UgCW4?cM^q}-UTL({~>n5_g-eu=6@ENG5fHw zS5_8jRTh48vyIZF+=Kh`J8upFsg2B{@u%S8I)F)?oALa(x^XRy+{ggz7$5)V=g*%& zT(~VqvVS8U6;KdBY3DA^{*)y*cjJxZ}b;B!oDtn0=&ms5e>U|*O&Pv|uQNJ;G-955el<+QNs=m*@0 z888O2R%tWiWN(kTtdR2Gy#N-Y#a~rJ^Uy#3g-ojqgm#G6VSYu+T(6*3FM3@yjRpA; zl%MBz^X;iykj3u~W=MgUNbJsn;?wT1c2bL==m$jf&mLW>&;fsf5d*M^4x;tH$n=`I2F%o; z!{C3~PVhhOKzQl_VGzLC_58SGwHpY*bC2WV$u((l@$3U{poEF73(Y@%94{0>x%Y4r z41OCTPz*m2?sK4qAOWe-;Va(0;fB+d0^Jn|z{;v>FsGmGh&QWZcnwpxJaEHpN ztgNh}UnUnw|8ItKqoBmQ+6{X9wcr9;sK=Tz9sa|I4}tu#;@&;cI)Drk{0Dh$u;=F< z70x!3RXackQBZG1vJ&C)@bNXAEXITIHB(^$b(_z8r2R(iwfc2Dq1V(C>Leh63u^~%8Nii(Q9eYfSNRQ03If4p>vZs__@_g!_@dV9}|-$EV^YT zAXi?V1vE0Wg^*MlcM)=M)L*@mj_2NJ#u3U_Er>f7fpzr;`3|b?5GL>%9sclyl0Y#P zR*cVK`TOENyboRo)AWJ?06(`eFlb`6w6+$s8ZU>!Lwmb89-elku&aI}iVusCCO|Ethf%FCU%Oh->IC$W=|*pFh~t`}1i`mU7pl= z_WL_fZi9)~Qh}I4?*b_PEEiO~yu3)T-Ppv$0=}84sYHL+w;-={NYf!F^}0N-KD=?8 zD)p$cNSG5S2_znArKN3o`tuoR-gier=yat`a;uvWWIWK@fHwd@=jq{*DVwOddHk`xykZL%Ia!o1k1(M&5zVcpvi(`u7*6DzE_$Q z85y~}Y!>aqD50o02$KMncZ^SeV3nZ^1X~0-kR^8Bg-OYq77!hv zd9G_eJRu?BA&1E}>lj_9$LFoeX*a1^H_**GKt00Acf^7AnL3vpU=9EiR{$$*eSLCk zBEjTBg8cm85LYb5oQ2St@#M)9vwE|qx6Jx5<2qimSCm|Moo!SC*yRixbS~J{6RCvj zL<&L5$H*w<*ic{ZIdcV_Z{r}UE!erzuYpE13R){RDbGCu0xm#W;7q#E;AFG{b6g)t zYXe{74TY7_GBYzndzSSC1ZHD08w;?i+@lXr&0O2q&>6|SL&<0R_oj+w-xLhk1B?Y` z3GirP{A3D-dI_}^@Hfk`Qe*lcK%2-0cSIz#G;&^B?YPS+(g9lAKwZu5fgog45+d&) z1Cfr2nHf|s0LVPPnYK3CzgL{xl@0&d&*tW4Q^L|w3z(;`&W7CXG_aYMOq!e zv?r{($nA&s3}L|Q=n_?MW0|Dq)uhI_;bmoe&=dk5SOpBa<1=lH4Q3035RjJkVRfNM z^OzC}nsS0CuL1ZWv?Os`X_k;fEe<+LI$`Nfh*!YOR9Xp0l%Q+|`x1FJmnECX0KF~+ zT8lig?e;EEl`t|i1m#|S1PA@Kp&>iiHo(Od%n8I_-Kw_+Z{KbMTYPP5s@B9s4m~j| zgBcJdoNR6Xm;x_y>Wripc_1q%=j`NEs2`x8@U|X<7%Br$ch+h2N=ydVe&p@#J#5U* z&JOLEJOJqxkHT(1NOFzBCHa*yNywxQ3Rgm0+$qRQ1o-%oMp)1s1Mla`85uuQ8tzq4 z_5@iOsL(54%s)#vZ{AdHHF{43B3U5j`gR++_r37d2UCC$Lqp0T`Nq_rTZeiZ)>LLG9pk+s`&1RH4JSEbmGUbN)IB zQ;73~5(;!MPFLAdt!0(KB!(Y*1Bn*|7CJjS3oU+PbGZ<TnDPX`6NC%sSGBUS(aYol7t}4NXQ{2$>f|ASz9egF>o;%Sz%oa7yaw+8 zQO+9rj=C!E5}%x&LKvok9=_QQd646wHu!ga{W%mC-oJkj`9E0h?nWyx3}$BLu@C2x z&O3iaD9wKtlHuBtLh!1Co(^qf$-xADSivKlS1I}@iE|) z^~ATH!NG{B1ITotfCo;%|NOn#T�O0L0*HNT?ltf+Ex9Nlh3)hDuAp&iwz_mZXYW% ziEQc*qM@D8?I8ENAU7zdIu+&wwXYhXQiOx^2^^uca`cWoAk~A?MO-Ft844Gi;kv$+L7QKenZE0KZR)k7ulV z_w2g`55fTG)eu0<@D59^T9Kf^kAHwdq3c2A?|pJ|GBmF_IXNwSWYBhVI|VIf$Q*iV z3!ru86zmkbT(_l?cE63hH&3*yPuom-6W^7w_qz~}%=b;H} zu(oBf5ol3v<|t4;VEQ!Ao>eZlNp;qewi%n4Btfx-g+0~4m^=5qTzYU(i)-5uh1^)Njv3j(`2kOzRsFg`*nb~ZNpqfs(T{WLHzXnOtl(iSES zp^C6Jy{L#)&%Uep@%PbU`6vTuJAtlbFb5{%^V?kK`YOSo8}i;7%Ga#Oop&sTTrZK$ zs1+i&vV~dsU+4q;PYzb+q=wOox)J*o6WUhkV!F7TtT^wJw#h&{6?hOx-=-I@L4H<_ zZ(N+8&*qMXD%BE%IF+;bOsGXF3?%iB@3xZIK#P_MM4zZ~uc@qqbSWgHu+1Q@OOmUg zrr=jie`FtpZYM~Hx;QCPzy9UfgmkG681su4O+ZNl{B_o^DLC^sbbCNgAasKq=Ic?$ zf%x-ZB?`z|N_iVEPc0x#VJwp1z-0zO1dJY!Ru+G>{f;E~Z@r$^2{k*r;;OLlr^j3G z<)JGNW|&hK#Bot-ImYfp=KALc+VDvTF_$48*eHlOKs3Z9B@K1lH#Rmt0lNS~0Lq+@ zP$TMX?D@sT&GCx7{7;w+cyK-en9wI8HcEE(Qjhw)cObGqgH#omxay$1w*C_!gmkge z*Xpie+a}vf4uCmcdlPyLXzkOkb+UqhldF;l0CWw$a1jLH-7(YTfc_?5e`w)6fl3G@ zeo%~)*eF29rizM*IfCW6rvM45l=mh(?sXi(G6m@_Xz=eB)u`9t1MsL;4(G4$ub&JN zbjIsUW|eMVT2T?g;pbISXlUB8!IF*R1go6`gU%JmH0l0w-N9m4R0eIuuv11A%P$|L z?E~BV_7-|3hc0Q5a2kSwjC}JLb_AqsScFKvd;RXv5|bW^B8-zD;O+!7G4DfRnu7jw zC=0;y(w|d75P+Ul<4@R#{ac03DE~;x$_j#ULub=>zlWf2-Ic3>EEROAwzLHV<|7bd zC?J0Utr5;9xSt(vpe;_Z4@+DEa|d;z%K47|wtOGvwFVO$59d4nf0ttZ2j@rHq>od- ze*GHtKuiI`8_;Jc$UP{NhXW?>7W0~1nrfm{*4Kwfsz3cr!Z zh;Cr^SwE2^=P?$i?|m#UR7S;AmJyDwgIs~7rjLDO#~u4jD4RfR~hyQ0JH#_7?N#OLWtN5A^3rK2XsEw?|KMa zH4)AMfZI8d&TywN2NZ{T$ zB5yP$+2fP&5UdKz96@q8V7}U|FD2P>n=5k~y+7T0Sl6q4SY}i;3fQi_qId9jU6u;|ZPcPKY?2ir!o4;aaafz zoXi3@!6BCS(RD zBfc*$>rMA`NAlh1XEiX`Z@N9dB5`)8P-arJ*tIa&aud-ib+udAN;{2Ox4Zoq4NW16 z!C^7@l!LQ--)8AH0yV|^$l3Krvdbr}AFXR^MJo$ZacrnKg*OmnU%g$Qu`BW#m}VJt z_#hT;dP@-nOF3~{&B!A62gHy_S67DQFVu#ete}D;B~Rv$E>@Tb(*_A8Gl3$eNUVSsaUP^uMm=<3=9#`h}v3TuE{!y zjq&gd>W{vP^=^?7FMk*Pny$ykdo@)XRE&nuciCs%LVuW#?&D9#8|zQU9^rPBIpame z$VizgCzMe+ohlV$)`G5Cifkr!T2HBaetPL1$G$M!O~Bay8iDAPxmu0=h^dMujNJc= zh8teZTcDFCU4vB4KxftxMV7z8TUdCb{^|t^Zq5wOx01)Erp$im2+>zpzyaj*CDTPP zcK1E3F12jJKcHr03|yQMk8B@KAd$(QqDq~MI zu7@WV>#t0ig*KF$?yewz|G7ZduA#`~D}sRxt@=3GgcLTT>=&pJT`NEDnvX?Xo-4)M z-nfUWAcQ9u=#XS_QASewiIkN2 zRE;HLzE;dg5iLLe=@K~u(~x00;_>57(X>3(H`Xo)H<`X&7P(`JaQ!-InK$Pyl&QS- zy77I5s^!8X&9j^%DbIuGU>zGPZRD!N+ zMLM(f(M}w)U~%bg3)a5Gv`<3ObokjGZqd$0Mp1a62)(ehTrO(Nw$alp_90}F?_HmY z|Iy5)w|-yY?bD8h{Wfxk^D4X0*oU6`xSl&A#%P$L5(T(FdgAZ5prrPf)nUk+IIbxw z<6oT6>eL{)xre?nS6I-NM^{;CogS!l_GB!Zxg7>GG3UHd>XDmA&{0*yJ$F#yu!LIF z&F-EYIr7zCSqbEorHb4kx3Wn+WFD~!>W<-HV}44izzXn}myLWA);=`U>5qmG=9e$A zRK7Nbf1cyNE5iQiqJl{2Iu2a;E-W#JP*}E@CU`lA>V|?~0DfDpkJ7O~U0=i}c}ujC z>(*(c^9eu%VmV}E;?1Q;U@+5)=Vdz~k^g{I$a}#Boy+`tDr|_9XM(5x{$|^=5x(9( zw<}vkli{SY&*e)0yBnzV^Z{_Ja&+9pi|AK_r(RE;lT75OFgo1WR`m|T?ac%?`kfS` zwrr80L7Oi-uY85vo``Bw-1Y3NZAl`yfmr6_;25v`bmImcL*V)Oa{uGuXE>ztvMz2B z4}F!N-e4~r&H7A8%gI@;_(}oq{(VYLh%xoMaAp*ZkWf(!g@EgS2YoRl>E$2t%Rk9~ zF0|@358e_JWhan5XcO?vO>lA?-o;g!N3CjaSy2n%)9GWPq70q83b`}?`e%nfzq_we zqTXQRG0(y-)eSUeInoEj_bJ~>6rAJzFX5sa>-E%AZ5?_B$qj>7xy{=<7tUj4E=?3G z3q3b+K9w?i|3xnRL_tvejN`(`{VH8Ujbq37nn>^|g3q&F>jjqu1MS ze>c=aF!A4~*;1W<>_ek0&Zwri)H}Z{9zyafTVYxACW5b}>4hgY%SWuJ>G>%;p_~2h zcje?C#BqmMPo|t6tn3(#Hzd|Lrp0npJbHoqenL?zf#2HHT~^S-MY9odr%2>88+4uDT`>+T_jPJjztZR; z5DZUA!*B=V>$)s{Wm+<3+`|NTq%_+5TMjZoc1*I z_{#w|5m8OOvb?slKIyi?8Ehk8yI#KZ_s^9147pusGMdKw7xvDO# z6XyJ`p$WG&lN%`oOMNxeFVx)EG;5>3S)~bjMi#_LsmTi?)8*^9m1x|DSIH46+V}5A z;(2*Rw4(flX_1iRC1fv~nV%gg$=|E6lHzxc$jMn;;CG~CWE?N^yM>*e?A==Cfg-%- z;h7PNK&C%~d0>-g{%Owf_U7}_HrsnaLNZ?Z5zu%>kXRsYa@yf6yl`_qR? z(^J)-Z(*j`&MjBYw2#+dl9LK17#h7fb$|oi(lYdXaksGG;4>pLFwv*#urVKx%9x{j zHVZfnZ+f267iheqF`h9eC)fNI%%Yt#|5~#lp}S}0Y>RD#0HKU@D7Q-;l|>TKf0tj8 znGOk5lyz~9Iw>=H6EtT!XV!E>vphT1b}0MBuS__xw!ce#aik~m`xZi!NkE79D<2a| z@`q1kc>Is<`GEoNu1v(x^k;@}?(DX2z3ENZ&8MXCy*%Hm;3XB?*+C-Vz{&HM2!skz zRp;zOmn)r#pA$lZ={MMmu9k>%D}8xFclQG3beVU0o^jf}ev@~+M1DGp>Nbb9Ivn&| zAg4IY>nx;DFUto3XZ%a&ZX*z=Y2-ljj;%Ff7nj=o%Thdo=4&Ih3ssI*MSf)te6!l0 zaxOA)S`+1WisYa{ASeeni*Kd~?Ne>-ZeZNF(RtY9(3i>n*Prfrf@mj5U zjyfYGS!TaZ*4{+!D|1}>64z`KKbhAld2JjXPeR7`#E}${!g%~=df1oxdzlMXyx08H zpqS$T&e&LFByz6p!PPP=+z$IR+&PGBSfr1KS3#eGntCAkp`ss9?+AFf1%+zi6E!u> zia#Q$~$h;w#aJSGuAz^vOJHUUjFAJAyyA1WIiOX{R&flAGum`u{Z3`~0>FAZV zPE2>kokqGRH7rr5!)Gi>JGqx}rLgH=x-(^x@~ zZ5QOO0|!^3ZSW_3-uT#B$ORmN^H_P7Q$G=?l>LRo|2|e4kA!4;ztUEtP-A+U(%Yv6 znj*^KDAqxQbU&J8YW}7(lz5O2m7Udo`=%%+|H5NXz}~mvJc5HOiZ7+pFeze_U;Tu{ z?5S6PtEAgX7b-&T6Th_&0(i&4#8_ETgtZ^GqL@-Zx6+{2X-Jv0q!BCg=RwWWkXNf{ z@+~-0h}K)KYD{*#SdXNU4%;aPv^sgmPof=^P^VwpE5ctnzZnE`_WN!S;drUPZ}6lJ zK}BYfyH=(vNFPYNyg^MJo=kqQ$?QlMB|@XdNnBD~;GANtsA;GFd(AJV_~bVZtHhVn zLiml=)^|}V!p?d0H*+@;VPRk;5u$9vv|JX7W^`oyG>)WE*^=F;G5&L|g@*%w>mG;Zi*Y2k72 z;QPL++@#Pu;t$6~qGR;TjF`PFA-}xg`k*{#KcO==*3Lw{27yF6Z%LA&h$DqoV^I*8 z(w6ylsh;k@Z3b3eOfMv#udg!vn?Dj{-gbS)D8)OF5p9F?R_}ao&lb$txb*Do2xq~E+X68{K}IK>k9P%Q2K+@d6WpV4yh*_~uj6yS zy*>@VTB#GE#T3F1+doQqeTs(So}RG;$(D#RxS zEJ&wJLWm{EP>AT{# z27jrj7{W#PpbQ+;b?qHQ@!deAc1yzz5CU1xTptKao8ySQwN;Q!(SgVl7CguEE(lHl zs+!Z817sXuVW}sWCJa4RPAx9c3NY)AKFYwpDO~9yv>nX{#OPW&n^Q9Gs=bDo*X$2* zTUutLEN- z#O6O{)aDkbpCcm4cx#+8T=$0bR7C@RJoLEM-;fRr`^w_&9tdk`*FvotX)ry_IXy^LI(@-2XP8l+CVn%b#*wghNPd?Dbk=3T^!@ z$L&O^phCz?zz;VfQH2CWVcYMzyD!|l@(@P&*nt#EClkfc8L-$Bg;!mz*a9|>_+P)D z2-eQ*w~!`@I~24fNoUX^2;B85#7nfvV+^ zoc}!W5k6;`zjkU0TzKcjw96~rCY;B20@%9+x~uL5?)k58(=DT${xlxeq!8v6m$XaaIHI zbr>mBkA$MZQ2I?pBb}+J;CB15K|ywZ|GWa6K?s;0gN$~BXeJXDnU%ebF#8A=i}~~} zf{&VCYxRz>qHnS@N+*M$F8F)ORAW(sFm<5q;HSE^C0fUu`qH`$%ChAav|!rHSm4$#?w}0S@tX*O|Zk9dQ}P_Z41*nE&;q@_+dPZ1pzEEi5@fF8x#6`iaUSu+Mh< zz||$|`wFdEG8xzlQGAY(ctmR?41Z_5Vb`8ykh?wz4q5vqRIo*BQhp?}LEYppcz&V7 z1p>b>$}Jq6N+^Warr2AuwvL>+7>CAmg$Q6gxjPG*4Dw(#A`%DTE8S|F@LlB9t5=L% z_*@{7pI_Z#>gAAKy~m(1I$D6_H0e6~A@p~j(|%gb557i8!-lqI;*ItrVRG01BSv(x z-QcA}#{p8*S)KIX^dp^&pOcAcmm7e`DQ-rh9OxgkV#0BSRD$0cBOm=`?OwXSRBxf? z#`@9}8!tk3$^CnxfRx(Y7`4_xK{ng*k9t*DC^;=3M^wAF;=dIdIO^nydJ3#x{W!h(sm{Z)!bC2>q&0lnTJ8lvA5Ox|W1ltem> z;XLPf=eX#FHOGy}Vwr!q~;Ej%th6=CG5LzUTN zS?ngkJ2B0Nyv=>JTow?hBXd_Xv}9^!bPAG!luLJaHNG#nc%_1O3 zNXN1uwRA4veR$tnf5824_uI}BbLP~XnKQrh`03^5qW+d;hPdP(I15<9{byC?@cGMW zI{1)^`b8`|qCLDHdck5`);% z8(gv1K0mo{4hoI^mDGxlv*R+0_3b6F!=1FUv;++Em1DnyLmN9RMNR8+Tq>8>4xzsOTfzylGdX%l|P<+Y}>Jl4duu{>tl1HXEkSZr=4 z=6O*K48(JJ^a_Y<1c`nM--ZFtyJn36U-e-br!r4=QLn+C5F57u8(3rLJ^Z(Iy!VL?rL>r%+cD^opC#C84pS^GfT5ZMPz@#8X! z!Kl^VY4e-w28d_qmvdpAATCZ2h({J^|1$=(pJoH?Zqh(wF~LAf1w^6aRDknAc`2|t zKJ*S|A?B+pwz5%_(|N8B`fS#p#Kq>~0?g=N3UK`ma>lxAs?F6fmz-=2Qj`UbKNXae zZg(!#w-xHo{dg)!IDtsW%=3BDQ9|b3yWiX`P{(1o))a&RUtSpiu9h9l5+NVYvOAkJpdgijc<)g2n6UZ?e#Se5lP!IN zt7RKpZ|MdezvW-z_p`FIM6crO#wec#DHAIa(NZ{HfjV;$Z!tJC z`^~{j{g{sr=>4VcSDlN$b+EJVT4`qtogGfAraGUiy@8zpC4qS@c03jvg|$LO8qG0| zl-j(SdxM-l==;^qR*h6onDG-#KMFjFnTB>#jMWdylP^?7H%9> z_eiaz&rp^1Ea~W2?6%+zCS(MiySG8SK4UkU>j2ZpUGiU~;*Q?7OI~Q+`7;c~Mk0}( z?GqbEc7j~bful-?OA@{zef}*q?_}PH6NC1zYRAy=Bz76q_;$VyZ^l21eOr&{S#^VM zD5}fIV1X>J_N~gyKaQK!)#c@3fm9crX9VtrIXWE(2@7YWTcb^nk3pRmM~})b&x6`o zhE)Vk(DHZQg!Ut=cDzL%a%1mf4tR$~KCI#rMD(<$Oiuo;A6~{5hsF9c?e4Mz+1f`b z@6H^4Ac@)eD$}#od%4vy7%hDqkekTtY<{~-KT+^p^=Q=Y+zDSzBdForyU9o1q3&7s zyA)WF2Ckq^OmuYh%$$2%xJz>CsHU&={N%4)nI4W-+dn7MyCYbr&l*x{e*+O#?60P` zKIQH7G~#z!_R$vYzt5v}uNB8l9lE>}IA5P-;2-H7u#ayE-4wc9iK1K&i)JT<{;3w2 zmEM$y)G~Wpjf;d=J$eRN?WJ-Z#x+u@XDG7MI7}w>hI#Q2Rd+4kK^9DzTw(ze722(32MtFkNTu2fUaXCqEQKXROG%-PM$_U_1^MM6tS z5;Z@s(Mhns^kf$)ScktW^GlP;D~79@6ba{lB`lL4BqSVZ(?1av9PE6d zsD9eeQFuYPmL4Mf>)~Z!OJP@ zd2DK<%_ZP~D>JLQV2Df(J<03yFvT(pJ~G7C`!x?dGo0!}XIY~WeavbWO|oTGdL1>) z2KioZtrVLh_+I0xp2ZhJEYl3nysv^mJ=?#(Gjn$M$UXn5Wg5~#mM9gzh z6^-Bvk>r=fro0rC){7Dc?^%%=IK$~o4|K7lo-?+=wOfyoV*H7hPsA}d4bd@ z80iRJAy|u)Fsz|%ZQwjJRReh4^kmxlFRkV^>G`w_t*@J>%^L*XMaeoYc0-kTDTvam ziXlEKycsxqcJ<(!HFg*(k~;x_8UCuy?>aa#;=)~pn~~AFW(BWO zDoInGik#ftVc;QxF^++2B+cVlI zLGnvDY7gX9l+Nir2#!60j`34;AFA!lnwzfCx4hZ+A}J(1mjTWE!Nxn~^?TO- zkpW4waAGG0+PDQnHGhs>Elr|}`1M`MG(3ANBRMmH|nAtCMZ--Z_@W#c~3SwL$%RO^%n2if}Z;rNr zxt|R4Y9@qPJd}{?Q>-waA?4?F!bp>PCK3{ND4K5GZLtl77Z;Y<8kV}fEWfp<;8mkI zRQEvkahdtBvAexp;C!9sYp#@zs1GV~?UyBr6BEVQ+p~4xu|TY zBa6Suz+gcaIP&s87ZNNbwM&dDs)3q@te@30BlEa71yOa_ z&C1VYWbSvEk%p1APc=Q6vi+8h%SeIOKug89+O*NrZAsFwm^Jt#b8Bz(@5s8#Ck5N@ zE_5kX=lmJ5R||U(Yn1ZI;JEh0M0CT85V}$WTE@~I%!vB+kx4@rQpToW#=pOBf5@Ul z&sEM}4BfHxIpg`^@0U>?SB=HG!J8`Qf1chM;q1;6bjZJ*fH$hpR93H0DFGQ>}@K!IH8b$+#nxLszZmwu!<9Dc( zeCk&TWkENqT*+@wBmayQf2wVu8kOYYW!@dNvbMeFFtR+zHaY7L44|F%XruoozOBt~ zr>b(VrkMt|3*MsaM|-=_b%S^bG}y1`4KB|MFwLvO~^=C{OooJDlcdlsuvsr^tziNolFCV7SK z)vEq5vz7@(lKa5H{Nf9O2u+I$;%3n0YSenM=s$+el=@?Z(3DUNbUDl zy&kl=4w;zF*27YeuY~cV1Iy+vPRE-T&W0TZ9hm^LRLeT}5G zXOwyz346N!GOMMzCutRGHB6(L8(;J(atIp~7Up+u74}kIzS4`W)x6HbASCf2*N+ec z+6^G7PKZ15FxV* z!W4mwxer?eMUt8iJa>_h{4xZL0c_Gvw>3FX>oz zww8Wmlb6kL8UcajiLxR(n-;MtulBE<~+ILe3wW@lHug5-4V<@)-P(bSBBX5$x|%S`od zy{C*CH@`UkvZbN^lG3!cAHs()a;!HSiI4YQFX)NQPe02G8k6|@Wt(+7(X3&lacy^3 z?qyheRw;dY{&A?UH+7KK!a{L5A=i0H=}G_8RDOfO0)s^FL$J+z!g%O;?U(YM%bmmc8k#4VRH$0aS1}=EJ^C>tcI5-C$0J! z#O>)4QpJmWw!73z#HaT9(|PQva?ysnblc@7RbEBktMW+dUGTUNX>ke+rKYu!4ft(s zmnL%q_>!}7a|;PA=m!|Hl9HY(<+~cOuAH9lf32*c%AfqrF(`i!c=H{1aKmRp7+*E;B`+|)zKBzVB(iaHcD*=@=Ev8N$aCi$ zgV(H_mGZY#k|asS@|Zw2zs@@j;W!jJrppYVy3%=^yO*FO@3!CctGzp`psbB+~%!^5Y_Z#1mk+kC*}`pVaWQP`cb*V=(Cy+hk`uK*+A zK%9oTb2QX*c35gLuLpJdDOHZvyuRG~3(IrS-9h&iB*g+YNhfjtlSb=N1is&TW@T3? zoCr4mcq^G$G8)cXx4e(>yc866A(1PoU(jQ~wC%+l0&v?(jkS{!zGq8CVhqqKrCn>i z_jKa`+z${wrUIzA%+)gMqO049B$aygii=g9qQh7rs$EX~qP#Al6QQwr66?n}V;=DL z`ojy_h=}|-+4@zSJE9?Ul8pAFeT6F4Z(B~`Ds!FUg5hm}y$$7%Cl{_<{--(avB@v z)qBP!-Ol&T`4|Eeb=#w&ssbCH@08|YB}u#m5OTrKV`Dwm38pHDhdOmMR+3)F@0BVc z?h;EZpJ8ZeXgGnNweNcGYFQ&~6RGzPwLL0s5`KZ|Y=|$KrvAufmYFx})K}uFa<)$t zNMvYIG@r#2w7qz-@3()0xm;{qXz8YThL1n?JGz8Z=-v7CK1R!|yn+m{p6koXj=%58 zcIK$2tjc(7>srl&VJ`k+i41z~_i=Emj$Y%#@;w7Ng08U+ZZdGPRbJR&Xc-9^Swvp9 z-x#`5q?+G6Ot%cc&bcBBkBBuNke`sT^v8@c5 zC6__$`RuQ-YJo5t6=jc8Ze^8cv@oFTReH6#75Gngs4kyB#KKfgwr~A3!Ng1{V zt#_J!bpkEn%}v_-hPD@5oG~brqq~A@`9T$}2ta4uL!!>a@xIS0Ye>{#Nr@Dk|El%y zx8v59$8oVIoK>R_z2N8^8&EbK7mSHd(sL7%U^w`R>KYbN2>#>(k*;&;8;wOifU13f*_Aj7{{C=I9IF7T_w$Z2WMs&mP@j)FC4-Zwme z(4;roZh85`svnz>EM}dr{C&N+z$!xUl{pr&YCf^96OsFzLoLz{u2hDj>~0eJ*Ckvd&*kF9rKLLXho=4l!k%^b1r z?s>9PGcqQf6=Gw5%ZZ6!u!Z3W*mqG&UPysHG*WlZAKdh7Ba+HX#D zYc|*g{sgowW>|!XrRC|(Fu-``UP#WKbL>7q8bebpe+;t8$u;gt2Hl9=91xqfQU|`^ zK-l#5Zh`Wr&ASJppYN-+tUXHZvNd&36|jE=TM6FgNiHs{g?kU*1(1aTe*mZwTW?)y z^$Rp2;*$$=KMMjYyr5u<{ky1pKy0jE+J>0XlNe!$z80_@qmWdRZKP+=Z~i5P{c)sD z%o+h$Z1C->=h{HBCcCbVPL0VXqq16kzu7CC=xmc_U1r;|w6l0hmpN%86?2@}QAzR` z|Dzv??}zT?iWiN%uzReCm+bXh)fYaY&hnnN7Gg4+{^O&l=bcUfc=fAV*{i;P!G$UN z)!K81BK4Sib2#*lBXr4%)-W1SZ||i)Tu<-Or){MRgzaM!M@}3>t^4kHeT}`HfQi2Y zfZYM$tLmOj1cOG~dUEf(3sj9Sz)@^;QoLlX4$PasG?2ll_2Dh!M<~?!cVdAI4rpy} zT(9keLZH;GH?+mZy&EsB1^>hop+Ch+F#kU;%B-HqMS_YxrRaF;u(%zY7S5YNr>9-XL zC^Gi3mfybk^-D|2*UIFuI zgna8Fp}-6dQHTQWuB)))Hc7&?)$VTFjPHu-YQIGd>5LK;_IP@V%*vmw z+ZC40B2ZE@`bfjs-K*O7+4>M$@a$#XL22>*xskmMsSQPYj2JH(k$@&AGpcJl8ksnf z^_N5E4PElu8B35e6*}a8U+D&UTndgqr;mKUmfBd_hExF%d{%p!+HdtrwSSPJc--8j z(_@+>B|`JTRaE$4Zs{J%^FkEm!!tj-iAz>+f&N4280)W9OfRseB_z7E|aq8w^U&*+g(P`SA931`1S5=aBQWi;FdX%w(5y zF=q|*B(dPNo@Y`1;G&v7JR~3ku}$>MV7E$67~JdNBjXp5V**EcdCvzQsU=&Q5EiOP zWP?cx!Fe&%sS$MaFw~uwBJ-B7B%`BM2jA%aRP9+#*B3*K0dFuH$$g0D7Ax&!D=Cpn z=pz;jw0$(BAWIhOGs_Pjl=DO_zJ@?Np{Da`Hs7M(3%^Rg$sAEnZd`p3cO;v5bkOg+ z0XWLk#=r$1aNa`MZefPYAU>*Q)w;z?`U2iyz-(J3-_*9*VO*A>F;4^Dw!S(d_J>fNaA3b$h%t2;5Ic2tnzQyjopr&yybjOwfOTBlnixR;;RVA$CUY6v_bTJ2C|pN?3}x0u-oS1M2zo!pqgw z(Ge8d9aR+|1Ufz|C?fzVD|;N|`(^fi8vED3&uoHj{d<2(zeDYgclAj{75_fEg`x0! zQ=8dt!Vuj}w7*B6PP>jLrBJCs9O>tc(KtL8Z0ywzGEVw(zWFiF(50JCs2w> zphV|dSWYaVPg5MASC1^N@)yLI^5=URRZ`;z3cocfzWAp{176c!tK!t~fuXOJKNExA zbqAg20o|mEiJ+Bh9OgdWMX2#+WWh_S`54y-lzV^!<_DGeU45;Z%G9u!_k!-ZS@5!2 zK0x;NKS=N%c|J^GHTp!QOblogvlH&qns${(WMVow(2vMfcy$U3;FgHq^HK$JMYEf$ z$F%$^y6r$bg{`3AE+~-!^_jE!{u$PfyTBzmxl0GzURc*XK-Vu`KAQaTStT70P?4i4 zXok)z9M8NRlImq>HDCs)Dg-iRHO~S@V40Z#CNUm<%ZtFY^jHXc_)SPMFGm&Ivs6l= zgcdq-MM#s%h*g2<+RsMu|C9(57#!v4c>A~*<7*c{j`YC5qM5B$ESj14GTe1QEPutB8!!P zO|SyjBDZC#nz^A{AgPRvo5AWfK*!)}A|x*09C8}O z@gcT#|CJ~Miq*vwkj1qOetaSZ6j=hTj+(2UE#P)Af`}OVV#pocaYK(bx{Y19Z{j6C zxhox!4XNWYk=*x_$d!<^S$r+cmczd%#S{vd!vU4ht!-&CPE9PY4Tg_82CvwoHlf?` zM9vQOCWNFY@WP>Fqzb7fk*DS@8}G)qG>znWHk1zCj)Wyb4R-rign|r@sGlvLTO_y{ z(63tPKP(4UeOAOx*(&f`J|KM4(wqaj?qLpPHkW%EF)LAkG=W@~#dS&6dSi*{Mo;71 zEGOBli6S_^tj;P-F-OuBkPm&VbqBM>fI6vIv2q~35+t>bl9wWT59%~0vHTCCTc|yc zBFX16fppwX7r=QSL$A=kFz4PNjthaTJxxr!)ga1$C6O4m%9~-$3I@-Kv7_a)_`7e% zklZc$9Ic*h49`f%6nGM3b8A-N^KYrCr!T2 zp$^iosQ+hNy1*I-7)LeLzq)m+)X`<#{}BE0Er4?swb(kk5XgG?F+H8~!ks}}3fa0~ z!~`x)Gh?q2$4|u>9v)VrOEa8TL(>g%u(N|mUZ0M4t&aXVx=0t~1Jb9UfAXk<$Y<-< zxZYilj&APW5k-juK&!jr4;rp+LciqzzVg3J^S@R6f0IG~FYf?{MM`QE1sHAg!1MpH z=KueX+)ALp41jE_VXKr&Ak{!RqsJxe?Kzl+vvuS zqdpLq^Z}pfD3>VU$-3B3Sd);vS=ng6trxn2KUn*SjpSBL>~cFx|I01>U-E3@FBX`! W)@o(GE($pE1yYhzhrnem-~I>f?*u*o literal 0 HcmV?d00001 diff --git a/content/project/templogic/index.md b/content/project/templogic/index.md new file mode 100644 index 0000000..bb1d97c --- /dev/null +++ b/content/project/templogic/index.md @@ -0,0 +1,236 @@ +--- +title: Temporal Logics Library +summary: A collection of utilities for temporal logics with quantitative semantics, including inference and MILP encoding +tags: [] +date: "2021-02-08" + +# Optional external URL for project (replaces project detail page). +external_link: "" + +image: + caption: "Taken from Alexandre Donzé's lecture at UC Berkeley, 2014" + focal_point: Smart + +links: +# - icon: twitter +# icon_pack: fab +# name: Follow +# url: https://twitter.com/georgecushen +url_code: "https://github.com/fran-penedo/templogic" +url_pdf: "" +url_slides: "" +url_video: "" + +# Slides (optional). +# Associate this project with Markdown slides. +# Simply enter your slide deck's filename without extension. +# E.g. `slides = "example-slides"` references `content/slides/example-slides.md`. +# Otherwise, set `slides = ""`. +slides: "" +--- + +Temporal logics are formal languages capable of expressing properties of system +(time-varying) trajectories. Besides the usual boolean operators, temporal logics +introduce temporal operators that capture notions of safety ("the system should *always* +operate outside the danger zone"), reachability ("the system is *eventually* able to enter a desired +state"), liveness ("the system *always eventually* reaches desired states"), and others. +Once a property is expressed, automatic tools based on automata theory, optimization or +probability theory are able to check wether a system satisfies the property, or +synthesize a controller such that the system is guaranteed to satisfy the specification. + +I have organized most of the Python code implementing a few of the temporal logics used +in my thesis in the library [Templogic](https://github.com/fran-penedo/templogic). In particular, +I have included several logics that admit quantitative semantics (see below), along with +functionality that pertains to the logic itself, such as parsing, inference and +mixed-integer encodings. + +## Quantitative Semantics + +For some scenarios, a binary measure of satisfaction is not enough. For +example, one might want to operate a system such that safety is not only guaranteed but +*robustly* guaranteed. In other applications, a not satisfying best effort might provide +an engineer with clues about mistakes in the specification or guide more expensive +algorithms towards satisfaction. For these situations, some temporal logics can be +equiped with *quantitative semantics*, i.e., a real score $r$ such that a trajectory +satisfies a specification if and only if $r > 0$. If one considers a temporal logic +formula as the subset of trajectories that satisfy it, the score $r$ can be interpreted +as the distance of a trajectory to the boundary of this set. + +Consider for example Signal Temporal Logic (STL), a temporal logic based on Lineal +Temporal Logic (LTL) that defines temporal bounds for its temporal operators and uses +inequalities over functions of the system state as predicates. For example in STL one +can express the property "*always* between 0 and 100 seconds the $x$ component of the +system state cannot exceed the value 50, and *eventually* between 0 and 50 seconds the +$x$ component of the system must reach a value between 5 and 10 and stay within those +bounds *at all times* for 10 seconds", which would be written as the formula: + +$$ + \phi = G_{[0, 100]} x < 50 \wedge F_{[0, 50]} (G_{[0, 10]} (\lnot (x < 5) \wedge x < 10)) +$$ + +You can define $\phi$ using Templogic as follows: + +```python +from templogic.stlmilp import stl + +# `labels` tells the model how each state component at time `t` is represented +# It can also be a function of t that returns the list of variables at time `t` +labels = [lambda t: t] + +# Predicates are defined as signal > 0 +signal1 = stl.Signal(labels, lambda x: 50 - x[0]) +signal2 = stl.Signal(labels, lambda x: 5 - x[0]) +signal3 = stl.Signal(labels, lambda x: 10 - x[0]) + +f = stl.STLAnd( + stl.STLAlways(bounds=(0, 100), arg=stl.STLPred(signal1)) + stl.STLEventually( + bounds=(0, 50), + arg=stl.STLAlways( + bounds=(0, 10), + arg=stl.STLAnd( + args=[ + stl.STLNot(stl.STLPred(signal2)), + stl.STLPred(signal3) + ])))) +``` + +The score or robustness of a trajectory $x(t)$ with respect to the specification $\phi$ +can be defined as follows: + +$$ +\begin{multline} + r(x(t), \phi) = \min \\{\min_{t \in [0, 100]} 50 - x(t), \\\\ + \max_{t \in [0, 50]} (\min_{t \in [0, 10]} (\min \\{-(5 - x(t)), 10 - x(t)\\})) + \\} +\end{multline} +$$ + +In Templogic, you must define a model that understands how to translate state variables +at time `t` used in signals: + +```python +class Model(stl.STLModel): + def __init__(self, s) -> None: + self.s = s + # Time interval for the time discretization of the model + self.tinter = 1 + + def getVarByName(self, j): + # Here `j` is an object that identifies a state variable at time `t` + # in the model, generated by the functions in `labels` above. + # In our case it is simply the index in the array that contains the + # trajectory + return self.s[j] +``` + +You can then compute the score for a particular model: + +```python +s = [0, 1, 2, 4, 8, 4, 2, 1, 0, 1, 2, 6, 2, 1, 5, 7, 8, 1] +model = Model(s) +score = stl.robustness(f, model) +``` + +## Mixed-Integer Linear Programming + +An obvious framework to work with temporal logics with quantitative semantics would be +to reformulate verification and synthesis problems as optimization problems, where the +objective is to maximize the score $r$. However, as can be seen above, the definition of +the score is non-convex and discontinuous, which makes it particularly difficult to +include directly either as an objective function or as a constraint in efficient +optimization algorithms, such as those used in Linear Programming. Instead, an +equivalent reformulation can be used to transform the score definition into a series of +mixed-integer linear constraints. The solution of Mixed-Integer Linear Programs (MILPs) +is in general very expensive (double exponential), but very good heuristic techniques +can be used to efficiently solve interesting problems in practice. As an example, +consider the following MILP reformulation of the function $\min \\{x, y\\}$: + +$$ +\begin{aligned} + r \leq x \\\\ + r \leq y \\\\ + r > x - Md \\\\ + r > y - Md \\\\ + d \in \\{0, 1\\} +\end{aligned} +$$ + +where $M$ is a sufficiently big number chosen a priori. The auxiliary variable $r$ can +now be used as optimization objective or as a constraint (for example $r > 0$ for satisfaction). +As seen above, robustness in STL are defined as nested $\max$ and $\min$ operations and +can be fully encoded in this fashion. In Templogic, we define encodings for the popular +MILP solver [Gurobi](https://www.gurobi.com/). You can create an MILP model and add +the robustness of the STL formula `f` defined above as follows: + +```python +from templogic.stlmilp import stl_milp_encode as milp + +m = milp.create_milp("test") + +# Define here your model. Make sure you label each variable representing +# a system variable at time `t` consistently with the `labels` parameter +# to the STL Signals. For example labels may be defined as: +# labels = [lambda t: f"X_0_{t}"] +# which would, for t=5, fetch the variable `X_0_5` from the Gurobi model +m.addVar(...) +m.addConstr(...) + +# `r` contains a Gurobi variable with the robustness of f. +r, _ = milp.add_stl_constr(m, "robustness", f) + +# You can use this variable in constraints +m.addConstr(r > 0) + +# or set a weight in the objective function for it +r.setAttr("obj", weight) +``` + +You can find more helper functions in the `stl_milp_encode` module. + +## STL Inference + +![Naval Surveillance Scenario](/media/naval.png) + +STL inference is the problem of constructing an STL formula that represents "valid" or +"interesting" behavior from samples of "valid" and "invalid" behavior. This is often +called the two-class classification problem in machine learning. +We developed a decision-tree based framework for solving the +two-class classification problem involving signals using STL formulae as data +classifiers. We refer to it as framework because we didn't just proposing a single +algorithm but a class of algorithms. Every algorithm produces a binary decision tree +which can be translated to an STL formula and used for classification purposes. Each +node of a tree is associated with a simple formula, chosen from a finite set of +primitives. Nodes are created by finding the best primitive, along with its optimal +parameters, within a greedy growing procedure. The optimality at each step is assessed +using impurity measures, which capture how well a primitive splits the signals in the +training data. The impurity measures described in this paper are modified versions of +the usual impurity measures to handle signals, and were obtained by exploiting the +robustness score of STL formulas. + +Our STL inference framework is implemented in the `templogic.stlmilp.inference` package, +and a command line interface is provided. As an example, consider the following naval +surveillance scenario: assume you have a set of trajectories of boats approaching a harbor. A subset +of trajectories corresponding with normal behavior are labeled as "valid", while the others, +corresponding with behavior consistent with smuggling or terrorist activity, are labeled +"invalid". + +You can encode this data in a Matlab file with three matrices: + +- A `data` matrix with the trajectories (with shape: number of trajectories x dimensions + x number of samples), +- a `t` column vector representing the sampling times, and +- a `labels` column vector with the labels (in minus-one-plus-one encoding). + +You can find the `.mat` file for this example in +`templogic/stlmilp/inference/data/Naval/naval_preproc_data_online.mat`. In order to +obtain an STL formula that represents "valid" behavior, you can run the command: + +```shell +$ lltinf learn templogic/stlmilp/inference/data/Naval/naval_preproc_data_online.mat +Classifier: +(((F_[74.35, 200.76] G_[0.00, 19.84] (x_1 > 33.60)) & (((G_[237.43, 245.13] ... +``` + + +![Naval Surveillance Scenario Result](/media/naval_res.png) diff --git a/content/publication/cdc2018/index.md b/content/publication/cdc2018/index.md index b9b6ec0..079c98c 100644 --- a/content/publication/cdc2018/index.md +++ b/content/publication/cdc2018/index.md @@ -68,6 +68,7 @@ image: # Otherwise, set `projects: []`. projects: - formal-pde +- templogic # Slides (optional). # Associate this publication with Markdown slides. diff --git a/content/publication/hscc16/index.md b/content/publication/hscc16/index.md index b013cbf..89ba9d7 100644 --- a/content/publication/hscc16/index.md +++ b/content/publication/hscc16/index.md @@ -69,7 +69,7 @@ image: # E.g. `internal-project` references `content/project/internal-project/index.md`. # Otherwise, set `projects: []`. projects: -- stl-inference +- templogic # Slides (optional). # Associate this publication with Markdown slides.