From 2f30bdffcb541e7f9acf9738b0da3cbce23b0ce5 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Mon, 21 Nov 2022 16:47:23 +0100
Subject: [PATCH] [doc] Added example for ACAS-Xu property 1.
---
doc/_static/media/acas_xu.png | Bin 0 -> 18001 bytes
doc/acas_xu.rst | 236 ++++++++++++++++++++++++++++++++++
doc/conf.py | 2 +-
doc/contents.rst | 10 --
doc/examples.rst | 14 ++
doc/index.rst | 1 +
6 files changed, 252 insertions(+), 11 deletions(-)
create mode 100644 doc/_static/media/acas_xu.png
create mode 100644 doc/acas_xu.rst
delete mode 100644 doc/contents.rst
create mode 100644 doc/examples.rst
diff --git a/doc/_static/media/acas_xu.png b/doc/_static/media/acas_xu.png
new file mode 100644
index 0000000000000000000000000000000000000000..d6de240a4a6fc470fc6a321de10ecc4a2a25ba17
GIT binary patch
literal 18001
zcmcJ1bySpV`0W4!N=S+{GNg1$hd3x564KqENDR_ofFK~9iXa`*ASoayC5Uu`NJ%Kt
z4fmPzyZ7I_*8StoTIU?*F!6ow`^0|s-Y?-=8uy3^XbBJq1hKLb>OKO2&5S@`IbOzw
z|MNA;RSo`g<*|~X2LeG-j`;^`HSp~x1mXrl8FgFN`|Y0@9}``@3;cilN?cq*E(Dy|
zNUp4BC*<FPbyfHZ>T@W6#%(XY%XK7hTGoH%jK@jJSC8w&m)M3_Ds3fU)=s!hOh!$O
zqPkYsBFCpb6fE9Kl$?6hWZwL4tT$EaN%OyPf9Zp_ey^$81uh{FnU^L_uEPa65z^ow
z5IxT#u@DH`+Z_l*aODka1VY|0Mi5@a(?yLyXi?b^ArPE|LU;&70`C9Em&>pIo&Dr&
zY3X*d|FD$M(FybAxo>3r_7^&%?R!%`qnXu-;p;O^Snj=^u5)7{dpJ?KH1lL`so^bq
z2;6{HQk8wb*PluB`e+HfixuhYyuR6TF*`nfI9#Y>l01sS+>}a%|IzkL;}i1+&%y^~
zW^s4v=-xy|Mh2Yh2OO{F(~pkYR8xn}H^9w`?(VJ*y=IV7c}H*wTQ-B=CoMVI-pZ=&
zwxRm}UNvXi|A$3ND6OkY>0en{UUoNC(zyd`&1tHrsAyth;^QMR79t}0e_7@(N%uu1
zJ-usVdIdP}vfvMJxsJ{Y>)KfVR4*Y8N#1KY*xG(YUvpA;xeno$cKxaR&$YFpaSvK*
zYKP^}nBScU#OX^Rp}W@1u)F6A1KIb|rJgJ|5Qsj7g*!~v;;jDo5uWa0o~nB;bVL>E
z<iDnu5JDmq8cdHBCL*r$%bp)D`0OmZX=kR%cOZg0lvP!y$}QVT<W7ICV;+7-+qT`R
zgETvxOhKr-cVRD2wiY_+^@_G(*)!d!_)O}aY?=iG1l*F2i;rjHx3#rJuMUO;^semS
z6VswlxVX4)hYRsAFE+e{eLF)oKut|8j8j(jT^Jq-V{dapVj^3By;=knuh+)-ZB*Rw
z)8oOx-kVd1%nCm9W)~}~!4hM!SS6cBn8*3g&p5oiyhy7~JAZ$FR{Z3oBuPoh*-w7S
zRqlH9$C&R3C8isNcOWG_fB*QF%pc(IKOX#k@^55!SJ%&-qo|7?ZEXs?yd^J5m~Nfx
z7GVOPc5S@E8YN=eL#h1jIX;PveyoK5;lIW1_&0R|XiN&J>)yZbzB-u8XWB46F;T%Q
z^jr{?ke(i})N_r5gyia)&UJ|CA1GvOL1pD&N5|bkq{sUYSy@*58xyy0-!{?Bm&M$D
zI1dkxxAg4U$pITL_EUMG-R-rJ;#6UKjSShD&!3;ZIUdG^Toj2-N*Z16d&4B_U+1%9
z_mPc-CEIzd6qS&gD&f29psCsKIF#pRlr7mhd5*|@Z`c2Brru*kuUJ1_+Q<Fy-+XRv
zu9VkCo!i3QMz25nn{#u8Ivk~hy7+Z+@Y$w@h7)7vL45+f@B(@U2ICs1+<(!WJUk*I
zA_-<F`8%0RIEXZj2M-Qli{V>qs;d_psL;=04KiWDxI`^PyqMG=QXLxLY0orGHbOIF
zF#BFYhGzdey$d%_)+bMJgH)<sVixT>6H{4vU*hxUj_r8l1kOH=ODdQc@2IG#SRKfI
zY4v??)VKyeGOw*k2oZeT^)34g%J*Pq(p+65553+snbzCa-S(`vw;;f8aIEY++Xs{7
z+ebT^$LD^M-Z4Z(mm8D1@ehu05KY~ha@upvi;F0H5^}O@RQIirW1@w4@MW#*iYTpU
z#@+ds32_Rj;TAbu+*l>l*|D2xs#9x<9HQ0Pf1l>zjM16*q=-@T+vDB&>Kh}^x2O@p
zV_o0b>F8*sl158&JJhAyjf4=0f9A`}yN7}_G;XFZ3EI6eAJ1$-i%)}-8T!R)t2>^f
zz7!h)&t7*#Gi@#{v5{V`<3nAO4$|O$;BNY2vdx<)*oZ9RE94y2<x5wuUX4qCK3~Hq
zll5dSSL#VYL73N{Uk$XPFCwwDn6RI=_V;UYQm(D9-@A9u!&IZ{$(dvnts;_)OnY<I
z<U#hk$0bBg$?@^R_TS%XXWuO`so!4umK?W#anf?(x03!O@chXBs`K--7Yg%-TMIMO
z)9?fA`3r^jzpfWQ5Ec|%{H1^-t8vxD#_CJ|hQ96e3aeoLXlKQ`BN7UL-}d4avWMg4
zx3>qU>pj99x?-5=lkf-I+S*v%2H)R#$rO0_bp4g?Z3XP12GKiT3=9Pi{)&Fam-XB4
z9U0kM9m-e#XV^z@ET|PRQv875puF|__rFlG*|X@x9x0g_m0R2{)-QP{<JVz|{s;Fe
zf7oxeU0+|H5qP}%<Ncjve)GWd)1$$``x>gwrRRswXZ@mkzI9Kgm6~Qhno0X9ytlgx
zmE`4BhP0nmY1eFsx_sf~d+TE|($Zm^?Chaoctq4Ud`7;1e>B_VQ+IX9{}L{)gt)lU
zJAGYUlTW_rp*;2MyHQS4A9>%1wVWSwZ!eqc<Y_tHOijD*!jqcv*fc5)Hv9%RKmR6V
zBD5vetmc4|+2#N#ZtibTKHOWQ<<7ki{?3%OoToL?&dYtVsz^-K)7BoyQjB;N5rK>S
z8M55=^}xUYjerFrqkm=Rh>wr&;birE&amD5XPh*lkgE(xW8+d)?Vv7d?~;Us1o(o6
z#zyldZ|w#d0fB#?4rb|Yxllg{xvdVd(AU@3)59e!93STH?hXa_2I=J(u~uFiq9%O{
zi=Szt&ij97r0l=bukIhr1zkXUo1CosG1>I*=(Mh`uDo2p+}wQC>u6{BPwm|3(2#S(
ztJ^p?tVLoCc$T-kU8P-y3$$1IGy1!_$}1{jMe=fTT;`f(pdtkH2&fqtjKdyI1Q9wr
zJC~W%5B~TO6Sn_n3X|N~**a!s%{JX}+uPfp{0=_4OjI^C`Omk7KoOmVo(=D-si{d%
zPlqmF@o?&+PQJ!9DynzVKHD1;RZli&uSI;lcI_H;_4a?!(h!;O;v8<B;)b0(#R#g`
zuV1^&)-^OBUFEUF(?{^=|7~yo+VW0KO?8zX93HL)G?18>I2h%z+^ejnX2bMAU;j0u
zjPKv+`ZBXmR>oFVR=vHw@T^^+xA;LB1QrK!vf5Dxx)U^KBcrs^(!UMp^>L5or6mbT
z$w%Ym?{jiqSf;?OWM<w#rb&1#LqJVXH1B+uf~_MsnIB=0Iy5&h;Ozgb`A#}KGV-m2
zN8WA=GpkXxgP=ugaKG%y1}uF4I~g6XrOeV8!8Ep8x025Awzju@7e1RpF&@l~@KjY(
z>jlulrdj)NYP13E9IM0{&<maB<Y1HE$H~=I4odv~76i{!wd2m;#?4AiZZ0lq8JXNU
zOdCcXFTZhR<;B9nDlw{wJLnwpmX(!7QPR;F&xyf0DaQ!XvI+`nACnu(%gfJn_NPld
zFg8A!Z-2Ql^!6>iy}kV^$_<UKsjW@+8H2zMSK_3s)P#*FDJeOF#u{oVdvUtc)ujaO
zvGK{K5D^6f!zbwNs|RNF?jd2{)1^2ZCjg-NPHn?|5M90;Q^m9+*+s|ZD8FBfbvjmj
zlbnKLLYo-Vpa(}r*s{vY%Oz*;-@h;PXu8hqlP};p+r70B3U;-aMdEL>v(2t^%|e^U
zaGPOD?iK43RrY@-Ym7g-82b1ey|_X_9ZCZ|JdRD3Iy6<p@xGf|#jf8(Wc}m$XE}=5
zLd(Z{>pFRAKAWEo+S=Q5r=sa4el0I|m_2o|g8jiXaM&Q<;g5tlPK$ku-My8zYLED8
z^(ZMRNwxL$scLOSWYmw!9<(d_3cw=r8dcxOx;Wbm+89GwSXj(#LcYBU50Bkd&FM=O
z&R2hPi{Gp%=FwY0>$@lWf6SZxZ#r%r9Ejbz1!Y{;^EYX`fZX|E_S2`gRaAOTk9KS|
z3c6|H)6yg@+b&fYz_nN+8$4Iz7IUHIkq=bbeiP@3woI9xHo4aIW~T9CM}#ee*(xmM
z>_mdAfK~`^SjWyT&xXA?I+~<iz@_8Gix;fy?9d7*$TIp}4ftin#A+dz*2l_{t8;R5
zYh35v^^u1sBv2wND=V#r3YwaxySlnYNB1F5g*a@IuZg4A5^^w0kJ2?Vnhf67jd=O;
z-lIo+?E-UwC%j~Trt5XK2hYz=!n@|?G6IbB^uDTx-%oR$eGww4lXrUJIVlnvCMf1Q
zNb59o7<rS2XZPUX;NL%kW`7?OlegH;I$So9Y1U=YtLy8kd=bh*p_VCMzMxc9Rrmeg
zTMF(#|ACI+=j&T)RMRsx^`?JCH9AiTQXAl%$+jm1g}<!%a>}2n+5@;H3}8RmpQ*GZ
zY!`qU^0B%aiqWSxZ>AtT=(OGyg+)b~HhBx4j1LXz<S{{Z2V>#fdN}z-K+V=RH#<8!
zKAr+!ulepy&l{;H)JVG_cDNe*{vs(s<J$9;luDu8WbHdF!t5d<!{g%y+r}e9L)M+*
zZ{*+(2nh+NK0bW2d!yX5quk2cnodH?L|Z#HHdeb+ObKwDk5B!gqmPdd{P<i><IDth
z6o4mDyL7;@?!9}RqoexE2sybHD8T8KDX(4;`1zecs~kOGfr|HQWhFnxY5fP!_Fc_r
zW-C4ui?+5R;n1@W9GWS5#VKs6348Tur^g+v92_K!(gw$4T?<=)rW3VugrHDs^hG{h
zw(fk*fU5TTW0blNFke-n0X7>e`5UIuySlpKCUA;<-|iTSXSUkiqmj*Ewvv`k88=vd
zPC||B7}1Mm(q$s<O3BK~f*$|vbQUI~`#L&_5AxfXtwpX1<w<y;(QL@nn>NT;hvVJV
zD2WmS9<Rrb9ezc|j^_AOJu*cfD4J&oirT8F7ia9ReGU8i>d=uktC@xZ0Eq`n@KpxM
z@||<N%cF4v;sD5@GBYzXSK0ObYM?rdE-K=Zk&(G`r~O_uqjK%$bp23kYbyjoSQ3w+
z`_6J7)Lbahm1WIt#P4EaV&In>8yiq<Na)35!a5>pgaMS~oo}7TCMQ4H`laY4^JaI~
zGxb64Se2WXmtB7DaDNEl?suumsE!WLGfB5vPHjue_wV0Z>g($#^O>&63i0wj1Sk$a
z$2p3LiCrv2%Y7&*Nz~7Ff6U<iWB5n3<40%|cTjO?QUhon+yDM?p4g`}<mA}EQb0+H
zr~lU>>OCIf@4Ne35SsWa%!43x@2R-%lZ(5ms^30;wuG*yt*vc!)OaKAec-Cx#i?B#
zvR^g@dJW-qz7Km5larH1iYqeKt0uwA&rBZ-4-e}$xSbvEK{0fgX{cGG2AH>sV^rfL
zYSTrEtgNW8Y`lpQ@jra5eD9vIaU(QDBO{}Y=Ty8#A{nAp>S}6v8tDyCx}~1{9qy$I
zwS-`)b)Az9JoU!G!GUOmHz?k_cm3M65%hf-nYE!6Io{6bA-NWs(k3^iUL5?ZyT1pl
zp_GZ5SJu>ga$oA9lalX?zdDACkQXH+jDR|2))M%svNG<^BX(9+2utV;{ev$nxJ8Fu
zR>#URaui`m04UqTZx}n?lq!kl8u5~e>Z7~mUR_;%y#ME$nWl$_NAZ&HWVvNR-2F4}
zZ&YdG70N+zzP>YG1@&Q>e=RITMMkF8aVY{nA;JQy2jzTgcb8t+PR-ZXS5I#QvS-nM
z)7bSB+e$2et*VE!#`3prxrP#F|Fl3N<>ZVS624{RX!K{unSb)#`}lCm?1}tbbHKu{
zUyBpr*%Jzwj|IX&O+!ONUA^zyw>P&Q(l$~=D>yiwNqx3I+Fs(&c&jy>nplG6BRn}e
z`aEpb=jHz9O5O386wHo;xvCieRT^*rOp;Pi3;{sP`=BxpQ%K+IPoDx9%94_jntk_F
z+-0I3#-5gWsu~*7G#=h017N}{CG{q(=i9eAfp-Iu-HYlbCiHK_9334uE_<M7Nln>|
zQsRYe2C~M?G#4~{eUCXZ{K=V^%sU0YfB(MnJ>40qP`q9)&)dFRh}RZosVXOP7w7g5
zAC~0jAAFbE%*oFeb}#!JpOP|O?_nPl6vWTZ@70Y!Bgw;o)YxCm&zPK=s>;?W$!%Vu
z6_-=L0)SNRWTQ$fkT;rI@L4<Z8sR~w1N}5pb_Ev@Qo_Q0y}gq)&Yfsp6<sYYxKoyy
zme|0(z8&0z<$v?-Fs%e0?>f%Btgoy4^7X5zy0SWgCfhAWFjFE;dA7^LEi$*b*l%<8
zlSaDa&BD06myrYFUDQ9++?Um1lRZ5>0hE1V%q%W;e)#aAwY9ag^HlKs!QkK^pu;M<
zgKlfMW2gbeoB1O4UDQ!9Y8FVjnsp8iVuo4RIarebn@2kz`k?3~^B8Ue!2M>J7$2{r
zpz!Q1eldYfWCz5LQvCNfkWvzJUl+E3d3pQa1DF8zoi*Tu&d$yzWDXXG0q`v@F8-Zq
z{B}W=82sOb29Mq3<V=x7ufcd?HYc`y<bVD8bwEmxLM6tv7+BbBKVI!Pblu!vd+v!S
zp!NSQ(b&dj5!(1#oz(q#h>yp>tgxTd<qex8b>JWz*kzA@XXBGFelV{6-rAb!C@Ux}
z-Q*}+u!>=6Y-%3O92b{0b8&Kt19%0@$hL0AeFqR5EMlVDGE~4Z-kJ%U$0ceDKaFVQ
zalUk79vqN`tgJwm++3@MpgvtMYoSEn3Wt)ao+c7LGxr_<_Uh`Y$&APIy&eQ&w)ZRM
z5fVVp#1sU@3AXW8bMj+Y?Ap1&H|hL8H#R=x=a2nX3IF4#te;CKXm#nO7&?n7+wDg*
zmR16c1B92bZ@E62Yo0lzfQnve*}k#^Wry~0C}e%rNtViV16tMB^*wv&f9r^_?Scf8
z_NkP=p*4Kv&&CGqKqv{*-;E6yYwMkk1tu9^5w~Aopuww(L3Y2B@VKkZCW;Wcy8ygo
z!Xi|AFE6hi@hX@CtE#H<^H+dvGFiuhs?glr44^vRvBiCfpz)g61A#IkguLMH?k;>o
zg4;5*3K-B14-ctnXm|}PSy@=_9FIVg(@YU~Z`ay%^0#psj|j8wwESFLJwroP9xLCW
zJ*mvl)@No~K&pNG_|aeX0>(}#F&>_t(>2ZyO7P1JtM2+Fc3lB>=!ZP4qq+Z9NMYeB
zpi)V%jg*80Phf*$Vn`+CFc=nQ1re91N*J{O=Ri%Ck&vh##hIR&feCdoSeTot1A1(S
zHG;Chyd`jUb{1y#gul(+-rgon-dj-^sJS+nOGp-uLOzvmoehG_E{JKng#EO*xL84B
zg!+F%PU|BCRF^Qt2IT5<JmNS<9zMQv=w#zfM?3v;bo#Au2mI#E)8z+TRDVBTLTHtj
znl_diRQ!75+FW>24vUo*1q%;zFRiE(<%#YM((>3H;DTfVPYu3fCy4B2V*Q975C=xF
zi(f`200IS=Bp6G|#^}EF^g!p^`aO^>`MPj3C=_O>!oort8XAZ<c)&|3BEFVMjSmdC
z!Ow4B5(5v1s1b+v06v10_dEFe$$RV9akJ@z2TuUS0PkD2kdm*NF?#S8IuX72;~OU;
zoSX%tZP1n{P{V_RMPo;aSUV8L=XzRN<-lb@lLh<-YYQ!N{pQV^!gjq5t%XfZO?M-y
zwL7u)`lx9jmkQDEsw*l4|C_g6Th6?!zn75$GZ*Xxm0w6m2(o;*NUs=1Xc(8dS4BkB
z9zTA}P<Bhm+7pe<`l~IuE0-&^Hje3p+<pumLi_aGj*kTnO`9gYVwj*r&;^Naify
zOKY6RH1fzW@j*{aBZQhKd|hH#)zQ|LHJVJDAt=qbIix9<=!k;Pdb|wOkosx3-~L8n
z&8IDzJ19~9WK2YgKL&guXx)+W=1qQXuISPV46sJ-EfLkgv!oFkjwXkPcVC<z$gNW4
z{v|Rshda^oFf=seeo(qGTo|8`k@4x%S^G;8KLGY$L{I;<lhk|!cC}%P<KkBYe@@0n
zAPToubSZ%cD<}bKrMtbo9YPKE+_WVyATaQ}BZ|&kOfpNCii!%jzLJT+)5EQfjA^LN
zot^i#DaT;_6aE613T)4N2!7y~T&L^i*Vn&2lmYr?ZL+3V%^C_kT+)JOv-^@tw>5^}
z8{FHRljGo6X?=>*XBqCNUsC&xbJ0Duq~s4|&v++hKk|N5Sl=sEJ&Yz}xjSrPy8I=a
zf<WRZoPy&L_GjQkF$)z#!F6f$%dofs1;y}P_y%w9x{8Xe9Od}BQbn_9Mj5Mv$k-nv
zBiF)FeMLL(<soc?*SdRpj4ExEA;K`5`QZak>9<0B05dSitJXs0OqUCKSL~ZWOp{F$
z7stu>`fQ<1KxO(Ny?i&6pM&$0O=CmDv!j&^sQW;;m^OIc98(<We|3%92Jhk;y8Z)A
z+vNG$x3Od-(&<(wX}xHGAR>y2p1uj9;q>$rRy#K*XZP>SoAp<;eB$Ec?d^BAcVXD4
zr^?p--C6J<hxJw1jrad*@Q1g^g9*qZzQUpd1p;@gy&BA%1#98|?=yZ}K9n0E_2$bN
zmp-SosDwwbJk2~Nah|$mR9&$DJUjd5&F~K&x_VR^d|JcEYKw{lmPuMmI5gjR0+CW(
zoe%(XA{`Y~$3x|wU}xJR`5T#krj&1FrkxZu2j=T-ZzK83()zmlES#kg0>Z+CmoFQ9
zbfG!fg)MMO6|B?GBlu$V>UHUBihuxGvDetxoVSvwL$PrrN{QufLno&sCADyM<v+^*
zG<gC+#`^pMuD0cDpRRU~6G!OoHE*BTVrO(|xeo=klE3VjEf!}7Fv<5`(@*58Cd2(c
zoNcN%<XtUr8GLfiZS$vc8INYjMJd$4?10N1cUblA-41|VfW8ErM|q^A8lnDF?ZnlW
z7Ar?l3tFuW7j9VBy!{**IiF^rMn-1yQ2o&(*DxA{sQY3UnX&PddC(bprU4D}|HQ|K
z#(jH8Q4}DWMoQ1yx1Y-YX}%<|+|N*v^3gRvGc&03Pj>cz4i@p}l^p<#fEnueUidLc
zd0~ciJG*6=;vPCWcB3T-LL=uD`aIpxZ06>_eE+xwvkz5RcP@XlV5@~{1&{htg{>Gt
zbq&s(z_W7<>1|XUM$aHoaz*}Tso5tdE32%E>z{)K7~8S9x!oV%KyGin?^Popxz`$e
zEaCm{C!`6qiK3W3ZF%&2ruLA`8^5+}9<|_W;Y>_SK-D22CJq3o3NWF)tqtl$J6gMy
z&4%du4>znD3JQuUSk!_7PJ8<mOu-w>QC@3cCK$$udXzt*FFbkjqy-q9+D9{WrMPKi
zHj(bEY_S<k52r%wyE2)99_>b7`9W{lYkp<)!~4LqBI~@@qTE=BVFsbQ?_VgmdlZ}H
z-#5?r_>hHh|LrAFXyD<A7&05TfZ8VV7wVo)OW?@*=eh>qcuG{)aSD>4NAW-t>g{y_
zMivmsQUkq~U>7y6VN*&+bXl{|$A@%RE~TUq75)AB`8nu0w{G16v2F%>u9w$7WLg~`
zfi6+U={4q?;m@9hh4Jv-l%&;(zdfReLh%@s|AZ0*&2zf(i7S+Vy3)(K*M#np(K8gE
z@XgOt2V;p^JbKg&6EaNUKz(?a5*FOz4YjN*#Y#(f{aORsmXcD}2g52@3dAryH01x$
zLupq4E`0v{8CXmG7KVz<dcczoF(4iFzm*so9u`3&+veti{{8%H^5BxwRqOM;YHz`#
zLyKkVf~04diwyhm<Hz*$bToiIAk|X1@YHc=beIAIDH%29=PBtTQn2)5GcsJQtc0w-
zgaPW+Oce@QcTZD-I|kO&2=*pRkq|huP)q7iADC|;kD)1cq0xI@Frek+umVX)9u6cR
z#7PfYaa*CID~gyJSy}z%EHP6dGAhc$-Cg9N^#UNF-@kuDPmJf#lnpw68)jl^3a$5{
zy?y>G8V^7>5YuNs#z0?((WQ&JhUE%1K0f*7#}q^bRO*D(NLpybZ`d*d_9vj|`$(I)
zxO_-T(zpKZ1GA#rLPw3$h{|oz(RL`~>}n~Q`T4c*>3J8s9jz%X^yBN+FM^*gb8~YO
z#(!}d$y298IzcM3;Dm+&JELo6RvMN?8<zjfT(&Dk><S5ooE-8Jk%$i5=)Zse$}1}+
zJ(h{aY6_}=)Bx(y-T2Oeb>-^3kzx9{jKyUvoIcE)1d`-GKs;-|fA_wVIf2B<%gZyl
zp8H+nt@!8H>++v6nRGbr-P_(`4hY~u;q~3q)g1;<1ohPi&>GN7D~pSO$gg5$>jHLx
z+oS>6m37y8mR0)g7c00LCJ-JzR#i<^*=t^$pVgNt>OnyVs`?%)`O?Y?5Llr9i2$zw
z;wdY+Ako6#zp}2g(lFK_d%l0aN<?%Dy#u4r;NszZ1f3$x=%Y)$i(6ah|M3FY_0b}I
zp~u2pvb}?O+>4~fsMdh^cUJn7latF}{)edt@C|I0jMSfTP%r>dxe!BiJ}5N-ga~3P
zu)mCqj6#Y)sO~{kIM|$n0kF2B!m!-p^LpUho}M0<cwkznb{O~tP#rMew<O-G+FE;a
zVq)Sms0kAUK}Sp1D-2Hi#O9=Zce{YSXb&Zpl<ZN*vWcW875MSiWwt4Gom}@FD0MKm
z0Z4*Kc>cUSiPso(F32oE&2$tL!Vu0-eHg?a2Zuov%K*s>Q36!yAAo9iUS53&zay)0
z7<eX=`0gEJMn8tz2I&_9F`3tR6ha@DkgBe+F+VR)*8lLw_&A8@Fab%)%AS|h&c+S@
z0DuTL!{2gRS%7&cH8jP=#lh2UC>@rTmXIbaS<tH0Q-yMEza@zVCAD0f`$3NY6dd{L
zm5`ViM;6p`B1UOg(sp3a*s=hQKG4<mKUzw*syKuv&@cAjKc7B*f)-{B{f0)^j&r@X
z*Gj&<{Nf?du8&PG%j+Dj6_<r|f#k5Py1^3;G%3IFN416-(1DDNjX5b*#Axa0C_qao
z-P3__NgV}p!TI?)QTyc(1)xAcdg;cJyEqjli=vmfzZ?bNmm>@Qr7EWJPTKI^Jq{r3
z8!F1nV@%VTMMQKP()(9H8`y`h8H|E`h7f0CV~a~7kv$9!n}r09j3f%Rgq^T+apBn^
z>j~bX4z^o?nE(JD0M?shAq5iq8p$9i1qUNm_ho^b)YHq&%j*f^+Q&BX_df+bJ*;bR
za2w{`tAvE{^sW1WW)GfM!+tTy_<BO7zrHY4d(pX2-_X!QPftU0lk_s+#4)JQtNQ?P
zmKGQ3W&I8E6d0rJt*!5%K+x;`_RT~0+?TD3I(Rv&puhnl7DM75fQ7?%o!3Tf==Vfb
zerai`Ct;)T6wIM(exPJkJ(_74IVP8CV2K8`gMw_T#b-eo=*cjLADOp>{<y>dvE5zW
zSXb9&7@B1vjTh{P{q%;2$nHu;5TlSy7l@re%6Fg@X<sn37Zes16*cFtfmF#7VM)CV
zRT!<y#sWYo>@}0z_h!|s>gwU19u;<}YxgY!n5}az;SO}iQ(g<X9q1qg$p*u_AG9kV
z8e#u<J-*_k1!KFqxSR?JL(AAW41#c9l71Jq{5^gB&mZ3YE%g@CtEGu&cQ|uIot19f
zFgGt%#UcimLM^o5TVi5Q;PWn1Uvme_5hhcSb7|l~;sPh3BtpC(0rzb;rKh);fv|R{
zl5mM;heS?}JVMz#<Jq%1K3tJ75T>BQ)|Fz<MlujWO9<eiim+v;ANzy0K390JmG`x~
zJ3I_#JN+Gt?tInqD#SRqoe(6-FQC23v_Jzwp(rU)8@|t;J~gOiN??|g%UCBDp*;Cy
zvNKixI@w944$3y`$fvIE?pQ{l!UY|J(9lp_YsSyeHpZ3v2VG5SA2CFCN<p^vRY3vl
zqHlUU-v-qNk}2|&qV6Ot@5ScDx#l@RB3ymHo)FR<ovRp8SBf{R0ssznXciC>MjBl=
zN<cC*TXx5>VW_?Reb9$_#+HVW+}sgiz%c6XJR5{B4f_pabInIE(5Q%E<Tezmp|=P-
zyB(yhs3wT2+Rii}pVfT)2n^iE#a{-BieCXKjGIO5I=xw5UIwNYDDxD#pyr&4tgN=N
zu>(kHA^cjWku_)$fI$K-&JG9(2w4AM>I1MwEiEl-A<;~7r8UxQ_xFj#xmr74V$_#j
zwNh0_f;#-FD+x(ScTp&DDJhEB#KaL`jex;#Lu(W4gR}!?3n05iAh;}3rfOXwSG}OV
znvCiF0T~a}AZU8R0s;asZi1&mOl)(iw(LI{2UB5yoQ#T!f->wQ{SM|KsNOW8AR}!K
zWaCG73d8G#gw}@g`(Y3orvPek4NN%0Lqj_U2N?pE&lX!Uf#Jf(e+eufEj*~HJ%P2>
z%#g)=a$g(}!1zSe0xsj_o6RSWfKda|Tq59j7p9Z(GAj^cR;2`o1_yx$c$=Os1}}3O
zDT-ye2YV00PqIuM&>~P&<DM%bV{2<`LqfiS$X^FZ3Wdkw`&)@PI)RnGHylUry`{|{
zo-qI*a?YouI)!~xQj{MXtG*uk-X$%I8=YT8t}rm9LqI}XGpw?6GmW5CQC6OSt_}z*
z;?*m5faiej_vc!i@`{R_HpVMpyo2r*+Z(*Sy9;neT~l)t_>kJAoBc4|ZqBv1+S`x)
zR8)eWE})V_?E}i792_rC{!ZTn2J^oMNW(($(<&+|&?8`)hY$w|=^Kdq7+KNfe9K!p
zb;_2Dn;Vt@h*<^(hTQ8V^9J#`hQc+EnZdzeBoq>2l01m|5v^Smcy<if8&kkG)?TeS
zLA0SfL495AXl<28PPPQeJ<z)?oU?V%c?p*+L-R!l|7}57A!|Fk4)nF2#Egs!sC>X<
zb#HL>zs4`O#zXK#^;083zHY$QVsc^<Kve^2be-SK|8V}L(4X$^Zj_CMMXRFr4>e0O
z8u>HI>(?{H-JY#;)d365jHH$Et@g||;DLbPA|s|22!2zUX$Txe7dNC9s3Q!Lo|g#-
zxcK>38t5N|p|U^+l#-H4Wt`HKI|JM`3xijlIhrg@*oLT;4&+aNxG&(^C^$4A++b&v
zm6R+VsEo;DKMl5|7W2B5N9o0I0uX}R&s<T97mE6riiU=r#}dX_aJ*gyEv?pNV!Pq%
zlqd>X5E*bP$_;|hw4n#Zv#ZC|2jc}tVtJQrZ@Ys41}>p@azTMGH<%<3@m#)yjg*94
z1GF=d1OcIuBJg=?N(za5_N^z=aInkl;eGO(K?h=5ICnycXoPGokLii9z)Aw!B;&g~
z4wMVPR~RN!GctkzM`1c#h$ezngx|WYy}Lj9(0_vhN6XxWqhn?U997I*Tx$SiL9l@^
zREH$3=Oa$L+1IGw;k6<xOeP?Yf}ZF8<jL5-`mSwjeCu(n3vd|%%}qovPKt$t{!t!D
zMsQ);&Lm<0s_8RaLNISZ%0dSJH}xrrmY-33^^+rf9L8&eZW-<Fxw*F3VVo$i@Ra1_
z_aFaB^E&v;t^XlK&^i=osWEh6C}bZfHeez{|NilG-ALZn!Jy-<v@&XODTL5Atq_tB
z6eFg9-2o?#{6}K0aV>JIt8S(VJz>$&`9XXMSY68TrHP97C>mcf+(HiNf;b6C2B^}F
z(Po*iUk5;IiH8A^D;we;m_9JtV2y<Ya}DGKs(Fi(#pdRQYMPXO_`sUg3&oCbz7?*l
zh-qnwj4U^AF!MGmX-pLHOT9t@AitOEhuB2yX@{c8B8vGF9KAS}fj72hf~$W$rINrQ
zC3Vt=ul#W!;4}q~B#%xk!H7J#V=yIhev6aqmA}7;e>J9SZafDa_`Oz_BQF6vRRnCj
zBX9>}&G9aBp?X^K-@oTHzb9;Ej_SrFN7lc`m6g95uJQp(W43(=EY(suIc@{+hERwc
z?CiX@7rP<n0m?KV$;1T`6*s+=mT|lYWYfExSs`-MTEt9EEpk_9-wb~Q)PWtqw&UaD
z{-;}=Fk-?tgKeM<xR@nhkHEk^9G2`LI{WWAWzF~f-y>+%;yX@7XMrWk&8U=8DJ+G;
z1+WG@LuXQP{Bj?ehAP>@Q7BYwESShzE<ksW*HXg2%2}t6P|y7;Kr|*QPhkjX8-Q`H
zvB>VlS(CKYCeoz#wSEawRh58*LpCF<ATyZHET?vM@SmF$Lh-iT-RBt9I4>7qt+{zd
zyj9&7FDu`Jys~Db>*fW~01Yin^7M(gnV|xV*|*)Drd<uHat)O=HO;FXv`c#r{TC|Y
zd&W<4Mf|Q_4z2_V7xd|;YO2jPzZ)fP^72B5VUYFr2HHG3D+?wn%2TM%i<_D_c$|mT
z2(9OMHfs0D$F7N7kBcH?gPJK`xQGVyF8JiH2_Q2ln8t>N7?GWu+ZoUp!FkFng5za6
z+zbkYQ#KZjaG<oKqn<hSfJ>i*HKSbMGywJ6&+)!?b^>dj2S|2iLh&XOXl+!AxDK>y
zvdjEb@xC*Cv(y+1g(F<vQcheNlmVDm>B-53Jb!DII%6S1w1Lqx;T+mP3+S~0IH=>p
zLQtyBlqFWwR<5tJz_6b7&TiM5RG?2D$QlO+2cRGo?%b&_&Bc2kgG7dfVPgY)k}oOn
zlM7AXe-$~e0SqTV6(}>Zwmk`;PL&u`JX?R|M8Tl`^y!GP8&2@A0>2K(;c5HM5J)_A
zC`Mntu=4Re0(+Q*gam{DaP8b<=#jhIWu(2H_*$Gb&HC)A+M$7J@t|~ULpiboV-rjk
z&_O*+zrRsB54{|6IE9@l@02cRC0O4OXAl{vHZ;{7(3qME!)BMddm}8oe)}b@8#UiS
z@x8yrdtW!13zz8INaC+wb$r<JGX*E!M4Ur_0P6T|5B!TJM}#PJIK0Zt%*@I{rgi|v
z9Ch)}hLwX<NKH!%1j3MnNmf_usYyGo9)eB2!{G(I7RJ6YmlpJTQe$J|sUQUtlbp}?
zBCG&|Tp*~pa@WIAKyGR~<W5@(-<@}s#&Nh+!x)W)^bKe&A5RGn4==RF%;A+_A_3qv
z(-IT}(Rk&`6;R`PZYD|j%Wiq6=;CD>j5{0ljW7t11As4MvBM0<LFcDXYkmCu)>l_=
zHrz#M8Fx{m+3j1)*Iv^gg7I3tBPWX<v}&Do+JQo)R3gldeD>>?63=qO)vLo|76w4&
zY4N}!=jAGbt4Y;gwlh(rBosID5?>lta8?0Y?k<a{kj3Rs@G^RvNFzu8)^bu|L?&?j
zd+!T^Et%~QnLx!kDO6y!4}M5dRzZr1xqB=$Tt(D8i`2&NxlEme_Z2qa$|Ycx<tt(Y
zxio#?l?f@a8xHu0R}k9SqjL;BSE-Zoz7UaFcH9b9C`5PEH4L_eI5pY%4P7Eq)v>~J
zw!-F2FtU%7m%n{`%@@Zm0LKodCQ-U0|K?LV{aHYZ=}%_0r{L?M-y=kGMrpE}7fGmP
zGnnY<O|-NyoIg~GZ%x2>^uk6$m4bw$qo!`!av3W#e=s#m)VLgTyzh%8{xnisX8RJx
z;L;2-7EruOEBE@)&&R2huVT!;Jqb6Vw-qk*I{6Jm&ZHB8^Hgg*TkY#Gg8;Pe44_@0
zTQ#EB^>;?Vfssm;I!pu3V6Zx?s;I!E1t=B+AdTb{-#zTpC6N+?p|6ezvG*)6lB<x#
zBJ?VQ?@~`9=xo8k!A3ZtW^>W81Hh`fx^99k=M^gJ8n^ziFPA9&8)dZ|aMJ88{qJ?A
zDI=t2j6OI!m;;-X4>(8B8MnVj#tMjtn6w0*fju2u-zGbHXu3CUo*!l((I6=CX|id}
zt_wigHA3HlDQ-zZ+0ZamEkasK3YK;OBmp2mL^*H^{)`hLI4=v`#T}*<0C$I*n;Q_0
zB7%aB|5BIcWE^1P0^GN=zn|oIuNNWDFf3yYWUr_*r)1i?ByH(vuwjjp9$2d)B2-y4
z&B_?ozy^b4VFCWv#l<COicA>sPjc;@prs`xbwL9m16bXS*)5=D4-O5Dm6{gE?1))h
z*S&r{8Qum^aJ2*22jHb)y3}RX!wR0%I*7D%eWEpCTnD-lmye5s12rveT1?E3Pkv7n
z(_5BZ>?Ck6U9z#U0oFs+2;)r!+8TER7vZEZBOGcP$R&{qmkIW*w*dkW96){p0~tT%
zn=>&!4pO0@kWeLz=`N}`zKV#<S-83JuRUL^u9*f*fYlKkwqQ!VOia9V)6(eS^AkaG
zP#U4}r3zZ(kpbUzGpm3-KP^ZMq5G`CKGMdKbfn3|3q~xkYd~i=R$h6a)ZgCPY5_A!
z5OmGP&E~1YD!10L<m&3*Ei7t~WwbGZNlB=jtoCyl=1r1slwscY;6d^_7cDE_>&wMm
z2+oiOd!jRs`p7fJrx$~xqroi*bo}YU9rc4?#Lpx=|F7lk=S4mxY86oZd4`Y|%Ysf3
zebfN~8ya|-M6~69E0eEpc^^LDA~Q5FkOp0{0kA8d$+aO9fJiSih=MB}<mEbgUik-9
z@L$Hfrl~@)D(veBg9$%BjNn?DaE1R!Qc(jVBYGnf9j}mvHkZ$+5lc`NNmC;$Z0x5U
zg>G5X)Both)gmXRj(!@{WfPfa&dGx0=O>RC2*=W5w28#S7z}rZVDas3Z5=&bJI1cl
znPYP%QjMkzUb3q21}G~iC@Ay?6h6>Q233u*5uBtQ*2CuR?v>fu)_uXu$O;2#pvI!;
z#BK%XAu_Ls@L0#iIh=TvMmXFD@apF2+1t}ow2%T+mOFf!=o2eEgafO3gFY1_^ehxA
zHI-H<+5v`UKv3~J7J#B*NbcEiyMp*Zoi-f3wT%o2KxSp$0Q0b9tkUAIU&x?VQf((E
zCm=0>(0Z_>hl@zN8!r^vS=^j1g?zStKOur47+`+ECS8V%-z^YJT$_*X(m=@K4d#HF
zsTdI!_Qi^TWTlQg*Am~tW|XZs8EF33G{Rs7Mm^ON<u9rqzzOCWERV#btj67dMxhM<
zZDocsV7}l%5u2WF%JA}R`x}40M*987wtXmX@%no0mOxf24^x8R<Dv3M=AzlZS~s-D
zf_i(@e*OOOzP&&@TffBU8Uw=_=*mD^0|)<PV_Xodr`6TF{c;!6&{zT3y12TUANUM+
zrir3Z$H(IdM449{W&_Tfn<=T43=Jt6OOqnPU`+bl-R%fc3JBxwo}M4-Eg~BmF*8iK
z5-83X`tK!){S?U9Fwdfaop~eX%Ff0H)MQqnsw?)u04pW=na2nvB0(*FnNRf+-e8*O
z;#yIuX{wkcOwa(5>q?&yK6(WBIM)_EhzO2zwCN~s3@xzcz*|F-#=M~;(>9<^x{2dJ
zOPeZ~nffCf%fUTOY?&lYS?JsI^j$23IyMbX+S3`Gi9zxQ-H0^u(!{477AJz#FL4|c
zKoEtqSSH*!|DDt#C5x5M?BGtpLOjN$xdS)(=n=>bdDReQR6?O$W68UF$~>jBpW)~h
z<t3UsHnw`7d=us62L?<Yz!550fwB#z*RK=as!222+F2=@q07Aihv;vr;3Md7cbu}^
z3_spu!JzE|PFw#rXxyNq&|bd|tSAZv{Q$W56cNWbn74#vHMBt}2T}=+wJ5QIAuSaU
z-PpBmX34aUXpXi)8w7oOO=Xa{<b8PrnYO10F7D0!>5z~RpgzGd<qeuNl!p@_gF3!`
z1-CL69Ag2m3Xs=;0<|_cxU@k1adFuIE*#8Y0e`0@d}g;nGT-|<gPGlXN=v-r-ixZL
z?ph<nJAy^<@k7HZs%;1euc3RO*a1E?GBC)=%Nz9<WoOR=x)E$baGly21w<hKvLL|`
z>2sA)#DSD7_01dZ#-hosBO<apUs&1Qb>PGl&RNO@h@7(z?%uv51OpfFtl%pLw?0tn
zMLxlA-WVGg7ywh0ocushF+@RDm&SYVD1^tPt{konV+Gk>^C@X<T@$s&#_k%3eU6Qg
zryXO?U(QoYRY1XTTXs@@0B07$AizgN^h8@j2(K&s4J5L+vM%-$z|>A`1kv-r$on%u
z&UD4HpsHawX^1wdb|52rIMW~s_THOZI;skmd*Ut4vdft`A{1TJY%pJ6CxcD^kKuqE
z;N@YWg-(v~3gn2OS*a+bl<&JGOJZflde-sDKNKYL*xxY3XgWXXNJd9S{>(HU0DJ_Z
zqRM4L2>B{3%o~(W0MXC@%$oft-rvCo*$gl(NEZ#jr|aqI0s9GQ9-f*y0jd>j+jym|
zDw2zr*A)6X$T6@9D5Q2^U^BRNK((bHCr2WY<Bqt0|NaH~X=wDkUyeTzxHm|?9d8VG
z4~#i9PaqyZQ|bKvz0|G-Dk&6Nem=fY@O=1u#E|<S7atuRfkOwQDo;^gzy1VB5HIXq
zkp2N}lhM=rg9W5Bn(1J5s1wHg;w_3+dIn(Q;^G8|aDGHS4ye$0Xlrj@)iMvVe7A?R
z6l-=_S-<Qj&{<#_nArRaIvt!5$*Zi~1}FrK1rjME^9e>i0NA0H;0+VA?jS-|e*8EK
zU<YCYR5~ahaDXNZ%7r3S4zmiYudv57q4nNdNHX;dS<~ZeFsA%jT{XOaAL%$z>&iqn
zQ|ESP5J?ja-e%PqdnqU)ut4Em;5Z&kiH&uG`UjE=*#O*A$7=>SY|{-QC>({r#m5J3
z#T|4Muo>^2vEj%Izl@C4)YT2J7oKZCNA#sYS?=*T1*UOg0VqATsEwAtKz?#M0*fsu
zAV4kR5VPwCW=LBL3(zZZRy#l~CDn$$0E!Fy%p<VHmXz>P5=`X7?&9I$!7?Tnc6N6c
z+I4_?;33G&=(kb8xW3QLWlI<Q01^#(EbKnCpPVTu6e=ix*%qMMlgx<`1w4_RUCh#N
zLDgl{OfrVkd*k?E#7tiC?zW5*Baa2nlZ-*yTWc_@xOfWKYA}A;+t?`43JVKE834_U
zH=qsDgG?L7PlTWAsvN*#9X-9ow6q>sUT$tM6hW&j{O}<`*5ykW8L+sCH-%svg|dQv
ztG>;mbU{fDt~8X0*M>oAE-^cJ;4E4ZPvuF0ciAyTWH!VIx?614l3re`5vYRU>jb7E
z`F9Hw?Eu}zW3MIU=jXqFKMx!==4(H)!C^$19e_`q5<Ege+n_O)?qN)J!y_Y!j~wAF
z44JY%mBUb8A9Rvv2B}eS+JZ?LW=61VAqj|xAfD|5`q@dKd8I{dkc$pF5+IxqG%PRw
zJ>K3b47~BAHzg&doFM{IO^ne*Pj3&{4YGk4<~uo4aNI!xC^Vo;Ax)}yfzSb(?Ne^9
zt&I(9y8sGo?LccZHu{y=gR&4b!=b`>51465$-LZLjNfQzXz0rq8#uoMJ}hD><M#2%
zNpfu~D<sPbwy%{NiyRpu4Lo+T#II7JoswfJIuL#{_dr#uB(#MFe|I?-@*(VewI(4s
zd9L0gKj`8d=%-jM&d6xcsSXdlIXE~{eXPi9yl8Ep@=Qa;0uByyPz%NqF#mkdkeh1>
zx=35)?4O{$tEm|s26j_;%=vqIiWnMOuip<|CZS=eJ?`vn3n2tSs06IjUTTe3H$;&-
zIzws6O)zLUIXk~eN%01?8;&(p)Uz>2laY~a42Al@cEbV5>Y5sG>ehkQ2s1e_oES+E
zKms@*AN_M&UkAGXKLXXvznD-;nw@GWOYwIfLd2sh<v8XwjhAtiq@l4fzhUKzFw7Vw
zIf~@w<h*?KDti_nG>k`T8O!Ab9BgHj_QuR+s9^|ua2_*CdGW}}T>xjjzrRm>8XiVK
zK(O4O!9SA)He6trnxMjqxz4)46=<!Gl!IM>VgLZ)+&??z*7fxTGgZue>u9?4{$Br9
z&)p5SH8`CHo_pIoYh?kVoo<c{N-8Q0^`5S%9}kQ>DD5cJ7x)+{^xBtOfdIk5Sp(k3
z1#{tfbs-}i=f-Mie06o=sU1*wRb-3J?28-I!x&}#IfvpB6VX3gv0y!k>25XsHARVH
z;~f}biv&%prRt+ADz=%7_4W5Z<1>*CJTMP{1ZO@Q#Bi{I-B6a+n?=7&Or(ZE@n+?P
zBdk#SA+tbNDB0uPNEEqu?_R1Gcw&*0RrVw&A{-nq!(f$I0^Zs8zeE3-+yhc=PlhhS
z6s`W?LG6bRY7Ll!V`0#&YT@*%vNez}5a+vld;BJKTAi-JTYDvDn}dVo5&Jj=1U70E
za8RclD1VR?z`xB-dKnJ4l>-Y4WCc*&H`v*iqg+Xdi9t#>h4Vk23$VgaK1_Fh0=6gt
z7QLgR0~8Et#{SXKq)*r8=H^=9*YFf98C_ika1#(X-p9Lz&CP+}*bO6Nq2e(hrKN4K
z>q}$46RNcR!OWhUmlyr`@$c#SDo~Q1K79((2jEVgGab?aI6(wcv<Mg(d5u5vm^KWL
zj(P#_jM0wPSIq0mB`xUbDeG!T5S(=TMvv~p_>MVSaDIN`3JM79t)I8|a1(y6K9qLA
zH1Uf0UH%9J?mFi00vO8h@bi~tWhuC`XtaYw3%wSiRG26}DQO={5*)Sz%j1~3t~2HY
zdmoq(VJ^m01_K@qWo1WL4v@+**(BB!KO^NcElxnvNlg??aJxf(DE51bZ;RoL8?xqG
zqFBK~VD5RJm95OV*l<}iBp6HUb{F+mWtFV0g+g;VmzX`tjWic`zMpuQf|V_<tc*fg
z2}Ut#1_sv2XiWkr2hYWw{k-qMas>d{L|kuzhbY2Z5F|)UKs7f5&_vnTDq33BwYB$v
zXYSiK=aC{kXa>+F08|tLO0l)w%Xt39YI}!;iOK0S&=&DS`i3>7I!|7!{ABZ|<JBxh
zO48s$EmtZs?N7IeqVJ`q9!6mm;Db}?@}<RfFx8__SFesF4`k{qFdrT1xn|0vu&^kp
zyDTLTnex=p+E-;WV7i)D_-`UAb}ap3WmFaVp`;k6<MUH;3Niu2+NCpUHdU3jN~0Q8
zV1#PdQpt{w0cs86%Aeh^4rZ|uG&I!KCObL=s~DaIVwhYgR7!z)%bWIWhL%x7Uq8hc
zKeHo7aN5nI_}zNbW9IJOU$_V@!Y=C9mqTnGo^9&favXMDyvqqjo#{>N%nE_BNEUtl
zgjD4?_3pNISmd>_Xe4sj<|*Q7@abvSB&{kV!a-=)x{jUlzPC6oE(o0Hh-i|KmmY@q
zty$T$Q7<+oGqtsU_kfSwCbIIaT#zghnU#~11Lk266C6g0M(Acq|MM1IzgJPgB|*f<
zpzb_+y7EXzRdst0Y-*9WupD^6pCw2n41}B<oZLt@4-^y@ej{Y70**33jElZiS_Wfc
zLXE>JJ7817Or6Kai%WWE_y`d?p}SjfsGpjODk&jh7<7M(Wb+m<9?VnFx9QMk6)8kS
zMI0yFM~iEdO~?3Ff=9>t_f)Hh6%Y<a;Pt|gOn^`hHYOG}H~T-rc?I|}ex|WmJKyer
zE~#T7HrpCK%elIprUfG$E2-9fayGVDEu}+39EAIw4$k|aLju}>st+tAD~<rz8lVIN
z=>+QPqv44V1@g;9Eq^Ee;IOWxu(yW3XbwDMzsqlga&xQUUrJ3W2=(}YB`<*i!6jhf
zSX^2vF>f*ReR1*M0c0?0b-bJDDe}FX4l}Qc%5klqcBf+1zsE*ZdHcz0DJHG&^q)m>
z?rT;x$m1jWU@<HqmccJvT!Q)I6E3U!P+-VnfdN6vMRpc5Ci<|fN_-Kz^la?i=Wh{*
zr)$n``ubhh5Ds9FYkLdRwy?0rc)2AzJNw`tXuT*K7nfdj!w4$9Cjm}HED}___f_Ce
z16alg5>)veJVJs3n&8-iQTjx^?i)V0+_;3OdoCFCl@oMM5s?o?MQhM)LAJ^<$0#Fk
zY6_s$Er%aBN_%h+KQA2%zH)<>2^S2-^n7<nb8_;c6#EHCQc&%IViXq_e{8^rKybvs
z3*ndwl2+QgyjQfMx>^JYjwI)aN;a`Xm^|^<`M5iV@-_cE_$~AY4g-u04#rJKUqNJQ
z!&{lj!^6T%rSF2aKM(y8Ob#2PC3N@D@XjkV+0;NvG9y7IT<rkI0O<fAhPuKlh+t=^
zJHIhLcg!(CqZbO6V9x>s?)=>j5Ag#i+^>(HJmElA42MPouo4v%Jeq&WRL4z#2)2gb
z0kYKs_OR5XzD*YM_YPoA2|W2DrlX_t2%_dE=`tVpT_`&s4F3ZkFXkkajLaEa8<b?Q
zM$I?yArO4?vO$Vme0&;eYSnN|@})fjAwmy6N%-R@3*cA(|M5prPUSdW5lMf!@@okG
QBnv`WQ3F+~VDapK0T>Td1ONa4
literal 0
HcmV?d00001
diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
new file mode 100644
index 0000000..8baa5b5
--- /dev/null
+++ b/doc/acas_xu.rst
@@ -0,0 +1,236 @@
+.. _acas_xu:
+
+ACAS-Xu
+*******
+
+ACAS-Xu stands for Aircraft Collision Avoidance System.
+Introduced for instance in [Manfredi2016]_, it is a
+specification of a program which aim to output signals for
+an aircraft in a situation where there is a potential for
+collision.
+In the rest of this tutorial, we will use the flavour
+ACAS-Xu defined in [Katz2017]_, where the authors aim to
+verify a neural network implementing part of the ACAS-Xu
+specification.
+Its low dimensionality and well defined semantics
+make it a *de facto* benchmark for machine learning
+verification.
+
+Use-case presentation
+=====================
+
+The system considers a 2D plane with two entities: the
+monitored plane (the "ownship") and an incoming plane (the "intruder").
+
+.. image:: _static/media/acas_xu.png
+ :alt: A picture with two aircrafts seen from above
+
+In the original implementation, the system state has seven
+inputs:
+
+* :math:`v_{own}`: speed of ownship
+* :math:`v_{int}`: speed of intruder
+* :math:`\rho`: distance from ownship to intruder
+* :math:`\theta`: angle to intruder relative to ownship heading direction
+* :math:`\psi`: heading angle of intruder relative to ownship heading direction
+* :math:`\tau`: time until vertical separation
+* :math:`a_{prev}`: previous advisory
+
+It has five outputs, that correspond to the different
+direction advisories the system can give:
+
+* :math:`COC`: Clear Of Conflict
+* :math:`WL`: Weak Left
+* :math:`SL`: Strong Left
+* :math:`WR`: Weak Right
+* :math:`SR`: Strong Right
+
+In the paper, the authors are producing multiple neural
+network that correspond to several values of :math:`\tau`
+and :math:`a_{prev}`, producing an array of 45 neural
+networks, with only five inputs (and the same number of
+outputs). We will consider five-inputs network in the
+future.
+
+Properties
+----------
+
+There are several functional properties one may want to verify on this system, for instance:
+
+* guarantee that the system will never output COC advisory when the intruder is nearby
+* guarantee that the system will never output an advisory that may result in a collision
+* guarantee that the system will not output a Strong advisory where a Weak variant would be enough
+
+Authors of [Katz2017]_ propose ten properties to verify. We
+will reproduce the first here, and try to check whether a
+given neural network respects it.
+
+**property**
+ :math:`\phi_1`
+
+**definition**
+ If the intruder is distant and is significantly slower than the ownship, the score of a COC advisory will always be below a certain fixed threshold.
+
+**input constraints**
+
+ * :math:`\rho` ≥ 55947.691
+ * :math:`v_{own}` ≥ 1145
+ * :math:`v_{int}` ≤ 60
+
+**desired output property**
+
+ * :math:`COC` ≤ 1500
+
+Modelling the problem using WhyML
+---------------------------------
+
+The first step for verifying anything with CAISAR is to
+write a WhyML file that describe the problem to solve.
+Inside this file, we will create a *theory*. A theory can be
+seen as a namespace inside CAISAR, inside which are defined logical terms,
+formulas and verification goals.
+
+Let us try to model the property :math:`\phi_1` defined
+earlier. We will call our theory `ACAS_XU_P1`.
+
+.. code-block:: ocaml
+
+ theory ACAS_XU_P1
+ end
+
+We will need to write down some numerical values. As of now,
+CAISAR support writting values using floating point arithmetic.
+Why3 defines a float type and the relevant arithmetic
+operations according to the IEEE floating
+point standard in a theory, astutely called ``ieee_float``.
+Specifically, we will import the ``Float64`` subtheory, that
+defines everything we need for 64 bit precision floating
+point numbers.
+We thus import it in our theory using the ``use`` keyword.
+
+Our file looks like this so far:
+
+.. code-block:: ocaml
+
+ theory ACAS_XU_P1
+ use ieee_float.Float64
+ end
+
+We would like to verify our propety given a certain neural network.
+To do this, we can write the filename in our theory.
+Internally, when provided with a neural network file, CAISAR will perform some basic sanity checks (mainly, checks that the network is in a supported format).
+If those checks pass, then CAISAR will internally build a theory, named as the original neural network. This theory will contain two subtheories that provide
+logical symbols we can use in our theory: ``AsTuple`` and ``AsArray``.
+We will only consider the ``AsTuple`` subtheory for this tutorial.
+
+This theory is equivalent to the following WhyML file:
+
+.. code-block:: ocaml
+
+ theory Name_of_neural_network_file
+ theory AsTuple
+ type t
+ (* Tuple with as many elements as there are input *)
+ function nn_apply (t,_,...)
+ (* Tuple with as many elements as there are outputs *)
+ : (t,_,...)
+ end
+ (* Other stuff *)
+ end
+
+CAISAR defines the ``AsTuple`` theory, inside which there is a
+``nn_apply`` function symbol. The input of this function as a tuple with
+as many elements as there are inputs on the original neural network,
+and return a tuple with as many elements as there are outputs
+original neural network.
+
+As our neural network takes five inputs and five outputs, by
+adding ``use filename.AsTuple`` will provide a ``nn_apply``
+function symbol that takes a 5-elements tuple as input, and output
+a 5-element tuple. Supposing we have a neural network named
+*ACAS_XU_P1.nnet*, our file looks like this:
+
+.. code-block:: ocaml
+
+ theory ACAS_XU_P1
+ use ACASXU_1_1.AsTuple
+ use ieee_float.Float64
+ end
+
+Now is the time to define our verification goal ``G``.
+
+We first define constraints on our inputs, as defined in
+property :math:`\phi_1`. We define all floating points inputs
+:math:`x_i` for :math:`i \in (0..4)` that respect the
+properties defined in :math:`\phi_1` (in WhyML, ``->`` stands for
+the logical implication).
+
+.. code-block:: ocaml
+
+ goal G: forall x0 x1 x2 x3 x4.
+ (0.5999999999999999777955395074968691915273666381835937500000000000:t) .<= x0 .<= (0.6798577687000000313588543576770462095737457275390625000000000000:t) ->
+ (-0.5:t) .<= x1 .<= (0.5:t) ->
+ (-0.5:t) .<= x2 .<= (0.5:t) ->
+ (0.4500000000000000111022302462515654042363166809082031250000000000:t) .<= x3 .<= (0.5:t) ->
+ (-0.5:t) .<= x4 .<= (-0.4500000000000000111022302462515654042363166809082031250000000000:t) ->
+
+Then, whe define the result of the application of ``net_apply`` on the inputs as the following, taking advantage of the pattern-matching of WhyML, and define
+the output constraint we want to enforce.
+
+.. code-block:: ocaml
+
+ let (y0, _, _, _, _) = nn_apply x0 x1 x2 x3 x4 in
+ y0 .< (3.9911256458999999630066213285317644476890563964843750000000000000:t)
+
+The final file looks like this:
+
+.. code-block:: ocaml
+
+ theory ACAS_XU_P1
+ use ACASXU_1_1.AsTuple
+ use ieee_float.Float64
+
+ goal G: forall x0 x1 x2 x3 x4.
+ (0.5999999999999999777955395074968691915273666381835937500000000000:t) .<= x0 .<= (0.6798577687000000313588543576770462095737457275390625000000000000:t) ->
+ (-0.5:t) .<= x1 .<= (0.5:t) ->
+ (-0.5:t) .<= x2 .<= (0.5:t) ->
+ (0.4500000000000000111022302462515654042363166809082031250000000000:t) .<= x3 .<= (0.5:t) ->
+ (-0.5:t) .<= x4 .<= (-0.4500000000000000111022302462515654042363166809082031250000000000:t) ->
+ let (y0, _, _, _, _) = nn_apply x0 x1 x2 x3 x4 in
+ y0 .< (3.9911256458999999630066213285317644476890563964843750000000000000:t)
+ end
+
+This file is available as is, under the example folder of our repo: `property_1.why <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/property_1.why>`_.
+A neural network in NNet format that should respect this
+property is available here: `ACASXU_1_1.nnet <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/ACASXU_1_1.nnet>`_ (from the Marabou repository).
+
+
+Checking the property with CAISAR
+---------------------------------
+
+Assuming the chosen prover is on your path and you are in
+CAISAR's root, you may launch caisar using the following command line:
+
+
+.. code-block:: bash
+
+ caisar verify --prover Marabou -L examples/acasxu/nets/ --format whyml examples/acasxu/property_1.why -vv -t 10m
+
+Take note that this may take some time, depending to your
+machine.
+
+CAISAR will return you either ``Valid``, ``Invalid`` or
+``Timeout``
+
+
+
+References
+----------
+
+
+.. [Manfredi2016] G. Manfredi and Y. Jestin, "An introduction
+ to ACAS Xu and the challenges ahead," 2016 IEEE/AIAA
+ 35th Digital Avionics Systems Conference (DASC),
+ 2016, pp. 1-9, doi: 10.1109/DASC.2016.7778055.
+
+.. [Katz2017] Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Majumdar, R., KunÄak, V. (eds) Computer Aided Verification. CAV 2017. Lecture Notes in Computer Science(), vol 10426. Springer, Cham. https://doi.org/10.1007/978-3-319-63387-9_5
diff --git a/doc/conf.py b/doc/conf.py
index 1eff397..b3991ef 100644
--- a/doc/conf.py
+++ b/doc/conf.py
@@ -49,4 +49,4 @@ html_theme = 'alabaster'
# Add any paths that contain custom static files (such as style sheets) here,
# relative to this directory. They are copied after the builtin static files,
# so a file named "default.css" will overwrite the builtin "default.css".
-html_static_path = ['_static']
\ No newline at end of file
+html_static_path = ['_static']
diff --git a/doc/contents.rst b/doc/contents.rst
deleted file mode 100644
index daa46db..0000000
--- a/doc/contents.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-Table of content
-================
-
-.. toctree::
- :maxdepth: 2
- :caption: Contents:
-
- installation
- usage
- modules
diff --git a/doc/examples.rst b/doc/examples.rst
new file mode 100644
index 0000000..028911d
--- /dev/null
+++ b/doc/examples.rst
@@ -0,0 +1,14 @@
+.. _examples:
+
+Examples
+========
+
+This page regroups some examples use cases for CAISAR. All
+examples will describe the use case, the formalization using
+WhyML, and the CAISAR execution.
+
+.. toctree::
+ :maxdepth: 2
+ :caption: Examples:
+
+ acas_xu
diff --git a/doc/index.rst b/doc/index.rst
index 7a26e02..17d89bb 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -26,6 +26,7 @@ Content
installation
usage
+ examples
modules
--
GitLab