From b2a917b33ec26d7178bdf4b85e518a6bbafc3d95 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Tue, 30 Jan 2024 19:25:03 -0300 Subject: [PATCH] fosdem2024_formal: add slides and diagrams See Bug #1220: An introduction to Formal Verification of Digital Circuits --- .../fosdem2024/fosdem2024_formal/.gitignore | 2 + .../fosdem2024/fosdem2024_formal/Makefile | 14 ++ .../fosdem2024/fosdem2024_formal/enable.dia | Bin 0 -> 2837 bytes .../fosdem2024/fosdem2024_formal/formal.md | 194 ++++++++++++++++++ .../fosdem2024_formal/states_complete.dia | Bin 0 -> 3692 bytes .../fosdem2024_formal/states_enable.dia | Bin 0 -> 3361 bytes .../fosdem2024_formal/states_input.dia | Bin 0 -> 2106 bytes .../fosdem2024_formal/states_one.dia | Bin 0 -> 1613 bytes .../fosdem2024_formal/states_output.dia | Bin 0 -> 2120 bytes .../fosdem2024_formal/states_verification.dia | Bin 0 -> 3220 bytes .../fosdem2024_formal/test_enable.png | Bin 0 -> 4776 bytes 11 files changed, 210 insertions(+) create mode 100644 conferences/fosdem2024/fosdem2024_formal/.gitignore create mode 100644 conferences/fosdem2024/fosdem2024_formal/Makefile create mode 100644 conferences/fosdem2024/fosdem2024_formal/enable.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/formal.md create mode 100644 conferences/fosdem2024/fosdem2024_formal/states_complete.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/states_enable.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/states_input.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/states_one.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/states_output.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/states_verification.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/test_enable.png diff --git a/conferences/fosdem2024/fosdem2024_formal/.gitignore b/conferences/fosdem2024/fosdem2024_formal/.gitignore new file mode 100644 index 000000000..b43b63175 --- /dev/null +++ b/conferences/fosdem2024/fosdem2024_formal/.gitignore @@ -0,0 +1,2 @@ +formal.pdf +states_*.png diff --git a/conferences/fosdem2024/fosdem2024_formal/Makefile b/conferences/fosdem2024/fosdem2024_formal/Makefile new file mode 100644 index 000000000..f99d01114 --- /dev/null +++ b/conferences/fosdem2024/fosdem2024_formal/Makefile @@ -0,0 +1,14 @@ +all: formal.pdf + +formal.pdf: formal.md states_enable.png states_one.png states_output.png \ + states_input.png states_verification.png states_complete.png \ + test_enable.png + +%.pdf: %.md + pandoc -t beamer $< -o $@ + +%.svg: %.dia + dia -e $*.svg $< + +%.png: %.svg + inkscape -w 800 -e $@ $*.svg diff --git a/conferences/fosdem2024/fosdem2024_formal/enable.dia b/conferences/fosdem2024/fosdem2024_formal/enable.dia new file mode 100644 index 0000000000000000000000000000000000000000..6ea7937404d3cb6f81748dcaddee77c9b5b2206a GIT binary patch literal 2837 zcmV+w3+nVAiwFP!000021MOW)bK^D=zR#~vX|5g`4}v7(cv49vsXc7f?pCswTvU`q zOH3$IMN;;74*S~|e8`q4QUVDAW5ul+dx|oMCP3ipC%V7?;manPJO*hNCh`3gTWC57 z;zhCyStWtk75qHE{adkgk=lS-#+uNt7Co6i+{5(mm zDBM|DaQi<$iu_yA=yv+~!(?*U!P3wD;=B4=KhM)}zRQD2>~Dhm>D*uZwMvs+yqs38 z>UN7HO47-rAKgzsK9ry7ZQaf7Q9oz;-ukOxo(BG3-CZN`;e1Hf+aPUryV)jLD4OKY z+mj|8{S?0s+SIKw(I{Sh{`jN)v3jKXi`Tx|9<-B4zVXvl7@yJ+a}!k)K`f6DA|``z zk0aN1@qSMFlbf3*7nvoOnk5%zvu%>*sUPO2B1dC24+sKcT>7;(gHRw$IMIJuxuMVaqng1Cq@_M|#<$k>M z)8*vTg3(}J~ zZzEKEKY8#sVe~AX$B(n=B+H+RwIYPg>ehb*(PNN@3;%Fc_kV(Q5U$p(&+rP9$nwzf z$5tbHya1&a;Sf^C*mOpKMM#a1;QXt26STk2Al_~2xs;^Riah;x#AEqL%{}q@DD=Wc ztG=w@XE+{VRXoDHSPED(9_^_h7kPL43vLqzXas1~x@t`LpL2-1;vgQO_#E_M0aXFeDq;6K`>VOH=TWHHLg--`iZ4GgHK-1<}S zH4M^!hH)FOu$6fQGr=oZ!7Dt=rpObzv}1V=aRgOLF&>DC^Wf{O97f;4b+qy>wsIs} zF^Ab|W2^Y!tXK(Iw?KkUo}=||y_i_MocU>*JatngM6v5x6vV4@3>aCY8^4B;yuk7Y zQ(Po*ELOVMk=Y45+y7;<7CX7-1$k16cazt@9?2Ws_tN%z>8W3$@j&C~$V?e!Y!fJB zmphaR4cWe{DcV9qCZHmNh|;zKK|{V$4cQq*Ll(bGsK^DGR~?xd(UDb#21@e#Q<5<# z$%d3<8W-owiTgY2%@V|(N#s?caC*-?2Mwc z%L&Tf2%$D61Z938C=+T(Q05>ggP`13P{zRUv_~^w5R|nE${l_ruFNQ0%d>56Kvs4w zmluSn#RYB@k(r+3l!O^}yrCYKIGzRZ^0G&%W0vHE$D62O^eARxFD8kvP%kKYkeIhC`AQXLntAYeh`vY`I}3({`S zA;5x6$0}iGlmv3N{`_$z3$hC=_(6R?dMfLL_7fgHKrZxsqJ~LIlJMD=~+@nM$p0PwG zu3RD$S1v<|C)*4XnLr|wbKyy11{E@yoZM|Pl?ky&5mC7j36&oTsMv^r3NcC`pZ1AS z0{PUCdc9THn@&f zo|F~PlQjYY+yLBkNhh`f+%#`C3^(2wl8tt^13&aS>_r>>UI#Aabl_6Xgi^SXY6dtS5c?0pR?YF4~ZWUrkEf0&D7YJj#V|r4u1^WLq8Gn6}uZkHKsiW@6Bb zpnFXZ#MMaf8Dj}{AOpiUsMXLb1A~6UO*`69G>TkpI#$b6otx5F(>AuQVx9<~ z2B78}*=^oJrrXODZ#CY?QET-;a9Po{OBySJor&I5L-$zLL4a;qc$ShZk~zm6~y>)QiaoT&f{pe zBN1vjo=5gI)5zYIWT0XikuxS06_24-+WSAvSFp(-BvA{-L<9Kh@ zsfs0v|BEsK#d&c9bpqtvjjtAhYC?r)dO}-Vq)T(qr z$+fyjv95hR{IwKwl%(OYF|^0Q1}t~zVd#B*#^UetBu#dCiyLDs+a}G@pJP;s^}~ z$#j&D)9K{n@IQb2`mGxN@ae<%<23%x{68t;$ANjrbY@?D96prg(|6a`pFe+&ve#K$ z=0%jH&(SQo{$HGB@wI7mJ^b`xFj($j9G9{EUGv+xEQ|E+xl9Jr_%Zo7yo*PFO^W<^ zIv&=ons%c+%ZtHFoP8XAb6@=oubXbJSNhq}_ftGc?usP-%iT3HKUyEt^;1%;cl-F1 z&r;K*e0|zz;^@czxzwg$#nXH^XujhHbO!OLOkd`&mL5xf z_uphxHsk%hjHlzc7!ST3{FHwgzR?gvLelZa;lI%8^I9LF>C8ak#shoG7qg0A;q~!v zqKB*NySw$C3-j6I=_E_)-dUt2ze4uU8%iQXj5%%pI?iU2C6BkGyqIp1gg%B;bzkAg z=CBriN_Ob`AxS3>rMq*ij_dp`FUCo+@1vs#aa8|E#t~OYbTYS!1A95>VK!zD`RCg$ zM0dXz-;OxfZ)>Z?V*4ZcQZB7F+^ja-b+wtvueBmq7)Oe8j|*?f5SB>YEMA*M$c|lp zrF|-UT+Lb=*SA}7^ObgMG~PktcX&P*jmoFxHbeIJgZua~&0fvtiKnySU{=0bd^Xrx zzx5wU_L7w8C|>p?hkt^NRljv@Dzy5;x*1)ahlk9?W2~)1fm1gk)Xk6~+>_~Jvi&Pf zrq7Sf<7{bVtHVERQM^oD#F%1Ek0GW2pML?zt zL?+r5nFxwlLtXqL(~_YInHH}pAQK?d&bbK4bau$}YnFc=J;X(6py`(^OP^-RmiP(l z%$sOEBUD8F(k5ev)piiS!7}2k_K*yD4W{%kzBXYM<}s>5&LRTgOp1-itFXR-a+I4# zPpL*+QzEI<=kJLyLg0+N(_~&RO&tlUvG{v=BkaK&9Y|<@O1`E^@y~R+&2jL~j)Mns z9K3cM#$!;VjNTRz7f2bqjADEwHr^#)Z>zB!F+z7kxwoNc-;f9@x(%}Sjkk7Q%-mcB zZG4Wc|8|g9n~rbeqR2nHtrF6)>)R}uPIhMth#Sz3Gr2cEaiqmjKAoCLZ`S8*!@te{ zW$<9ub>ke$ykdTXw|`wBAny0l?eC?V8N{^@)Q^-FoiT?6!W=eVr@{zncJpSJ8zD_V zNdtLtOhpjV7b>J>UqTv_KuX#gT9(o*l$7o=LeSFhPfKIa(!sQ}S))cw6VTE38$W>vFMc>Na5lz&+;h;?jQRNp1 z2^Gv*GGwX(LMbdPvSX`P?K8birsLKD#f?GkXlhBmIFhxRDK~mr|2*63@h>pAM}r6V z=;?xctH}}9o3U3AXeXmF>Y>CqkdD?XI-1a6I$DE{1|5Bbj>f=&y%$Jf(9u41w1Yq5 z?mJU#7?k1wLRy*`QX4`BJM7LBE_n4?VBwuYI)=I3%NT^~^gw_>UMhi0%=&aDq&G52@6%#pkNQFss;rcOu<4`byx+Kx>brd?7(pkOam!R`{FEhH@UEn!_ptnl7&z;`5T zX)RVIAxnm#Bm~IBuDJ*$As15;;y;+@Vnm`36>USu+Xyi^_Ep=={j^@u7d^g9BjpL zh){lmf!hGL(cW!9GCG{w;E;?C?KVi~ojCP(hy5!KS-A~7R~#6JQXGAZ5M0MQR2*=k zg?HDX=W7!bM{w7H`*IyDkmq14jzfg<8=yGAZ5*OFz-UK`aciIHO?(fQG*(y13Cf}yvy@| z$Z5B8lkPiXbVQl3b6-op%s|`i%+y*^h^QNCH^^XSBaxUe=5sr@V~CqADcW8ov7_bQ z3k>GgWn`3;gx%b*n|p(cs5J~ZXfyZvn|W9O;@!hpf+L0lAdq4Fh%fNRtVgVn4uC(- z5pFgWj-<(smU{tcVIB|&5NJCBt+N<;2m-CYS%(E6(H8)5yF7&Q4nQp8igURDARcKX zu?zq}8zXeXN^AUKZQ+Mi;0M<&0sL&j4|XC*3;4lK>q#30p=fn zTtjrrs@D38wUl3gK7c+h`K8?os)hd2PVv?c{QOvqw&BiY-Ht&twJ9N_HLX%Y2rFxt z5f)2ue5(P z;bs+KrV+*h6NpCtO%E507d{tmv=P6dSHl#0V9eo28=8-Qn~^oE<^)HykSQ4Y`~}orq~vX zP$V$I5)sT5lagtv0E_^Px`UDT+q)cKgfB~{oeYf*5Nh4gxjh;&Mx{WQ3vD&)(EtHx z1UfC~37QTx>Rd^@v~$QW8mVUY39oja=!i>6xHWt9_LJ67MSlpv0XW|T_BD1nd=0McGaIftwG z9Dv08QenQSkhXB7q_IFM5h6Y`bgZLDn=wPDp^LW+!)bV z)j|zdLXC5z&nH(FFiwObK?&oW8-7HoknGsKW&lT!EIWs|k-C%{R!%F^oR@c;GFt{R z4Zz6Dc^{{uM*5)3DFH0O#|imAuaa8*-v@KgKSq+^@2;LP}^r zQo_$^Gdge*Kq4PVbfUfJj9=JB2-3)-Ma)(PjM=u|1))PA5miERWT1fyiX;Uf0wC%k zP;;Vv=uBKzpvK-K(`2*fwKZX~*@wq!!W_~A$!x$Q55byK5hHn7xoo|t^qbe#gsJp9 zIGwElivWu*HJj~+8!g`w{ZsyB8ya=4J0|ps_`Ty(8vUVvAu7H%y1QVVd<( zUCysa~XW~dFL8#tfGnu`rK)&B1V-kR#bCbKeqk>AGy{ZlQQ1N6~^hP^vP$t zJ+(HRmU`s0c>Q*sAg2z@f4Uq-XZ`+jvH9)0*}x$t?$a!5VdB2}IcK6?J*$dx9&*{$ z(gg9Q4|9}W>g?nLH)T_9fvn*;f)`DfRNM1V2I{K-d9m`_C zvVdg)%i7MeegT#hfMv0W0?PuH6_8~ug|7chCx6D1wE*^lW0770*et@{1K4ymfX$AM zWaUNqaN90+y)v#XZAe5~Hlll@;K%b+J07z*R#)r+mu%zyFW`=!%iNHFa*N08i3UKJ zK17%v_ZgsV_hm{QMgz1K-L3^QK-yfHDYEufaQSDK)Sy`IS5xtK0epA+@*?kv4yk8*C`1 z!1_u>QZV8Bvh{64+|tVUD~*)-OhPIO^&6K*4A+-b{W^eHW+z literal 0 HcmV?d00001 diff --git a/conferences/fosdem2024/fosdem2024_formal/states_enable.dia b/conferences/fosdem2024/fosdem2024_formal/states_enable.dia new file mode 100644 index 0000000000000000000000000000000000000000..6c0583cba82b13b368811ea1222e096c6919617d GIT binary patch literal 3361 zcmV++4c_t}iwFP!000021MOYSZ`(K)zxS^&+-s`vTjXTg!3@yB9v0ZeboMfrK(-Y} zJBnn;O49VOfBTY>o!GKuQ=-Vm4UIN|9g0tsAAj$Y@BRGC*SmD`5Ettt&pu9J0H%{T zo9BxpTYjAW=g;3i@aZp~-u=8tqMzjdWf9#?^0U z(&Ro^$Cv+$(lol1gD$6^-c2UE6D*=KQlD);jmok}X7^=0$)daX<8&6y|6UgPeYTj^ zqc-E_d72lKhba9xeScHErk9&(F8Ag+GWRN4#Bwi3)(-*&93dnh z1{GX@kc4piO!||Xxh0pnC0Dp5m#nW>c~KToQXZ0=<#`%MSxvPp?&INf*7GQpEOu;J z2CKM9$}&H3|2I*()>%OP@$+u$yK|RCvN*nR_eONg@|Y~j+v~5E9#=j4lcm`ol65jm zm`vU0TPpT?QK`R!Eb{c^b>H`KFriiZV{X-xZzhvj{;h}S3BY=2D0Ot+h1m#3b3 zbDZvjsXuB6>xx7gJ;lXl`Y-WPis*c@N~0{FPB!2126QITyi6Xp?{*$bKKpMxFE{J` zQbyS#Di)Iuli%{M(-$>FDj~_@9A7dQxU^AQ{ZNZ0JM zS#$D2-hPxV)3_$U0ufS01kfuiwI@U`AXC4F(Tvmh?s}dV*`b~=(yA&76`CBb>{(h7 zgSl_xWO-Y5PYzLln5bV2?Tf-b#AbQ1h>KH80Rf<(euabr$^kPXw~r1dHPe1H*0=fN zb&L9YTDG_2(B;dH)7XN4#$U^wJqR~@5Ss2m1Oj{^zx9w(iyKi=K_N$q5Fp}eOH^<+ zkiSaxI8I2O#+a_JwNlmh#x=D14xRppAnekr@~mtlq&}bAM0ZL0B=0B6*3-$ld{S^N zp|-yCA94B+m&rWZ6)gSl;9&c=Zb}aJU&M^)J_Bkq;Sf?y0O+(K0Wc#ZmG5PC7q@?( zadv;Vd6t?~T7`eV9q~}zQgctd+zNJrN5~Y9piry;E#uLa3J3we+P)EFsAAyJ=tn}M zRu=SVbcSezN6?P=1;qBXql!v}M%yY9{?Ms zm{N=dpaP>1hvM}M9|(Y#Ki0Kjs^kv{C>H3)5w}uyRMeecX1t~_{mXBa};Hin60grgV%}^*4+vT zIJl42zx5Jg+2T4Xiu|#gDnf=+U#D@lJnryE-S{<(d)oy&vw|?2wIOwCgF#VuVy17mBjjQIrvO zq$mroD0@Y@uc8dSz_Xss0KKAYO;PTMBSGVX8p^*xh;X1Rhe0S5Ash$^94a-FGgc9% zkny1*mn^%Ev&HFRUrb{^%y4x>Crw7%|(;pSpt zMP<~DDMRxEBNc*E%Rqo&r8Uw3hFn}BR7aK7;jK_Wi&5p))pZSHCx;>3VO3yxvs@oo z_JQRlNRqPt6(20@iGakK-+9%`D+o+CgRG;zaGMEGL zIC?3uua~|=bG9UXG{*x+Cky&$&e=qBtefUtMmZTlN3Q)*z=4AfV<^?uXa5|i>ALXG zb*%D;Cl7f4+}rcdNt@HaK}W2|blb}*K{|q)9$z?c(Icv;sJurZji?J|-B31MmsVA! z*Jmi})=+|*Ed_}H5Hfh~cKI3T(to^3Wm*Uk%6|khOoa8+C@wcWRYo`z-U=VX3fB-p zYy>OZz6g>;o<$JCPDGIDy1WSTB4}I@^u>!H>;4?%MUeAkrEruAa>RZCxk>~PjKi-`4gYNq;dig%20=RcEb(tw(e4rF3QGU;5eOMkfpUe6n+Fi(!83in{2Fv87VO5%qmBJRF^1 zK@Ugg2uElH?Z`!A47S@CgZai79*$11pogO~E&GY^2pWkjjUOnf1eW9dm! z&oiiGa&WcFQYMIwqM`~X8mib;P@xkA)#oUA{j^VxlGjfi>8CzP$!X}BjiZ?o`w;{)xTLmB3Z!N}pB5F+<3U@(oU!W+%zwC z3^!s7&Bl7zLF`5ywyKT&sDsc7ItZ;`LZ#ej4f8Pv4>w1(8>8y!&`$aE9l-gun71Ge z24_W1>SMLkG`OjaHEnC_>gEYN)Oe`*PJWx$Q0ewG)Sz)XH#@-^ zu?sc80o1gvZG5!#P~)Md7t|0Fq&bFDR-p!;Nh}`jo+_wqDB{9~3iWI#=xr#EHu!s{ ziN1m!o4Z+}|1RQHR77fqmJ}dt-q1rG{b#m|Sh4_N#uS}RF@J{1MHq;oxN{em(WxAu zMKUj~HVZI(ayqG~*kURwe8#CQT)Du+F^H**p8MkP`|r;4=|kcsNmC6HH`VJkr}I|N zs>&wo6KOD(ks4XVBQb-^Ou)}R70`Mk2Bjm00p$V`pF=z_7w{%cR@b+Ak$jWv6s1R@ zZfeYGl*!UT&R6qcz~DVInp@Vga3m#^KhjQ#VVLzg3$6bza;-p8&n^IK+kz z!f*Yv4IYWk-FtfLhn=ut)t?)VlM`dTO{$Xaa1*J9u<8^|u~5YvF^6t4V}N$%95l(C z)Aa0qfYO4%L|QKdV}OPC^m-H;p;_xeV98Z-9v>%$ZCwMQK}Z->zylGlVoQK;qf5iH zWqZZ4byD;ICQKd1g&AR4-bJrwmU(vE*5j{tojE^NC;G%7s zO6R}8RlG?Nq((i{@}j)eH~|H;8m8%w!ly=6At=33Cn;`vUl0FU)HBM9WZxOu<6r~S zJM=L0x;|@(?#sN$@5`1j##p{hkFzdRzR6;MMr5c5kk#-RD2P_>2_m87bgG+L4^>8|XeC#a^lfLFP?2A(ER} zf;E@g8n!AP098VP1A4_(buoQ^Da+sw$@xZS{3rzq~0@~nItU>dTTL*F{9gjQ3o8nHP$DQ1B=gTKMU^)`G zvQgMq)ZY}g&%R>IzNlhf47Tix-LY@mY7d90TdOoJ&%T4XGaQdQ#hcwG@uZ rtN4xaD(=Ip$n$DD@YZkB=qWBfy{q5I|H~q}`}FSrzhg2wviJZ1w}pom literal 0 HcmV?d00001 diff --git a/conferences/fosdem2024/fosdem2024_formal/states_input.dia b/conferences/fosdem2024/fosdem2024_formal/states_input.dia new file mode 100644 index 0000000000000000000000000000000000000000..dab3127fafb7528e06ee5e95a36bf42abb8a2c78 GIT binary patch literal 2106 zcmV-A2*vjwiwFP!000021MOX1bECEzzTaQr@!q;v9|)wTNvEB*(~HiWGuxhPk8Bj1 z7J~zU-sgGs8h-fk^EQ|~h&b`1@OBCuiw6-(;x3X{NVZgd-;DI^X)`l5hm*FcDhN^-S_kPUUrak<*2%`+RwhIqq z(%#&1Tyw#==HhY9`N?7z#c9m_^xWh!iUPsI+-e%{MRz;NiU)FvHFc{;FYf&`jV`qR zo(IV_9mqd^UTtkx?mG6p=7oDwqNbKd-%B@(&zgoSul-3=?GJw9F9T84dOu7DtNv-2 z>dW6whTboi_nZxRZME*fqk;(1-aV}Mz9*6k)9kcNO--Ak*!+i>>i-mL>7t{_F5qD_ofO}30Xh@DO8tk!+0n2>%fH1cE&BUs%0rLG-sHQ<&(Y`U z3k{JZ#P@Ee{{g4tRqmmzOhVz=fbF8^S%qhIx&PFeE}3EV zeuE@+LSzOVb?9bO1Y)~bMR9me5{BqfR(*ye=iPe75Za^ejqul-w4rj;t@33Qdm_Hn zbYKAj@|SB9Kqzo}nLEXSiyX9_jbsx&E-HxbWiMWhIP;gab;V-)OMFg`RvRo<8|=H< zAhr;ZYXGT(#&vhF11;hLdh=q|w!5yqR1L`mKT|4G_tj>^{G?oo!`CqQ2Dewop`tLY zGNeAA-1Ds;JjwR(Fqux0^htrU1lIi0-$n2sQh&vd-AMZuoGtmvg-OBb%kF3NbP~3h zh+T}8VW3ts0?^NpB-`t7E2_Uy5$?CeXkKZh(%H9L6AxLF%B$j~DR>lALcLK59neBE zDiwA>flAM24JsK_YM6)ymEIsK;Q_dkt0n{1&z0QV6&|=!Vb-9ML8XR?Xi(|Zq0(q>7Cerl$9k&>^{jdkh;ZG!8G!0BteeS;+YcQr zuA(rMb6qaVyXPe{FM$Pl=E=AUZtFyQ4IFx`HY$E9)lgVv(PZuQ5kF>>F=J(cjyeQ-)jPe zY#{toa~@Nz0BB3Lqzt(Pt5_j`4plUkcFk^8Bf1cwcV)Ejtc$e;6`^-Jl2kd_R=aXr zs?zD-VDJu)9=yX}FL-yng6l7aT9^NIav6dFa`8qH%(+y4R?N;wig|$U8Oi+qBr`O$ zS9_L|Z8Wn+&0ND7VgH|$NEXK!(=VHqAv-su=%Y&CrU1ESA?!NhBRO?$+txdx7 z3fYQv%htO4p^%|q0FNM8kCHxKPEFQ_;SmiJ(WHI6nY0i6!Mi##xO`z;#Cy_xNj!))uF_3@KPh{s;qG@j1HdYu&97X}8cGn-12GTWLUP!Q5K+t9Y zLI)xPMBnH}BK}H1LQ3rFWdlS8h`uT#(w_}mePe3aI~yK4Gp$;PSd7eU z`E~=TmEAf+^A=*~{#>(lh+f~;;k9?A9tezH%}(VTh$nt}mjOk_m@EI;(7`s-9#C{= zj)kNnXJ%7!oJ~p8|Hl_(Ml8+S5KP%Xm?D+D0wJXG)OED~@T%OkYX4-Jc-uQ;mk5>! zB50*^+3D3}aCZ6MSnPPrRSi|QKJTACj}!;gx#Xe6FmX_zD^h-m zC3yZS)te00eax=mvRLOMR>}#Xqv-6z3-&Ok{QbW1c`IcW(8k2Q9|TvJctwwNX&S4H zYPQL*u6#(?z`9_d$uOo)_{Ah1jBs~xMa^8P6l|juI_4eR2mWrciDLhYoK8GwgqG4X z6I+{+Bt%U{ZAOy)QaxC*Ay^DYyZsyL{fi{MLA;|F9vCBrr!|CUvj4xS?Ehar8Rx0} kUQI=e%`u*{ZHz5H&z@I$_u=G$rgtCy4~v0iRrGuS04qT*>Hq)$ literal 0 HcmV?d00001 diff --git a/conferences/fosdem2024/fosdem2024_formal/states_one.dia b/conferences/fosdem2024/fosdem2024_formal/states_one.dia new file mode 100644 index 0000000000000000000000000000000000000000..bb3d5f4662c48c875f994b41b8b62a637525785b GIT binary patch literal 1613 zcmV-T2D14diwFP!000021MOSgkDE9Uf8W0Xv9BpH7z6Hhx4M(Ax`&fay7pfB5;?(3 zxDtqrv)T0F{`Q)WY{G{_fDolBs7(YJW;|x*_ZyFw4__3Fs%t=1Xt;=6 zKlC2ef4_Ws=cpf_?moCac`yEZjI0!KM;Iq(kLr^1_50~`yWMKRE+#x;THtTAm`?vE zK|rQLXsSNlDax?|mvE9?%dZm7nLpofs)S@kAJsWoeDhee30*al%Hz`d(C&8P1qnomopP&(7tcQDQN#G3Nf4joKz8{p+uCNX z$9(s6;ua(%TDHE+m$TP_rYqCF8%X<$AN%uw){Wi|`Nh=lE~CEubW-#_+}<-9GHp_N za2<*$YEKW|#&>Dl5N1UgiKb;PHf@^qvfQ~7lU*v2b!s9YJIZqPpQ$G(I#SjF2_sd> zpK%U43R!UfWq)=wEz$fxy5PCLpE(I#!d&H@@_Y2E9?B3=g!t~G`Zp-fSJ^|MOh92} z!q(ASRGAZ4_P>fAGS%~WSu+!3C!rV6Ogq%DjV4C&`CtGI7-*s!$yYa)lKS3~%a!A9y5|vdDQg4zPNeE5bly3EIv^ zyo|Q9nmV_c#OncPdPpr#ds9*I!noQ<(aJfU?&Dd!dO*ezDrnMfJS!fpEP)(++UF6 zdZhgbD$!f}P@Hsaj&1SJ)GcV@enyLMR-5*En)XOT5bHgyl^I3aeE^`JA+c=p!WFH5 zq%_>DYAWtiHFsUvcp)bGBMAJpSmRaM$mq*PR{G@dz+_~lT!b?&0x1`Xm>HOidb@TG z7n!%mMK?nZ5J7|>!~kJv*wDtePZr>pB#Yz29GWbgG%W=R2(mCnuDAqO9Crxlcb~Gq z{IHHKU|+UyuEG{h$`+1hLf|+LSaWn6*}^J>de?$^PQTAmKU#Yy6LXrx@VR2h0A@e$ zGAf)U!BFw<5S^ehjN0E?(OBrt2xHM!Zq+b)s-6Wj^iHp;3^|5%GugO~>u7Nig`tRb zk(6A!&ppc^riv_-HSSS}k)JC!Zf1;|87+{b)n!CKe*+W0~?JYvy?*R%*uy?*o)A}+i-;=(H;u3kh< z>m0<@>+eOEMqEjOr}uuN#hN$+Vl2|IflYg2XWtLDX6g`QQTJHTFuRsLVK@^Z)QGhO z*XlMcp$Y6{EXcH-jtx7Jev5T^40SJ|joE%9*{;|B!AIwXS<-o47lzX|hxMj6^r~50 zL&vtL?14$qF^Xj~{9@vjn&xG@}^F&y_--rzDjP2T{1x+}aQ{B-vN L{`EMIJ`-wawh}F^EbeANDujliprzgvQj-4coEZ=*u zVt4+JLGC_fwOn-rYmRt*ER|tg3UCe%IVgj zA4Zc$$G@9?{G7g~^PJ7Rz~>6@gR^y4k?Z_b&l<>=5M5Xw+^EcUe+Xkwk|fWE3z8Z> z>ivu+r-~&}u)Y8I9r>6IDgWZct7@RNLXy1`ZN1=9j+`4mn+RlagpiyJD!2fQF!(Yj z?ZvIe73YsDE*e*y7cUQClthk~T#8(Uq3=3DCN+s3-0pJXwc|?@yQWqTEk1im65bg9 zXUC75D3E=9^tQI1yN$ffb;m7G)Npz7Hpy=JMbmU;+@CdZfAnH+<-1j*_kv_F_Rqtx zFaJ6zdY?}3X$={-+VHU9E_G@9@UVUGHg0^w%!)KMoOU_c{MM|O>6%VV_EjlZry_jk z*^P4cpWLks(c$FaJ3%;|$5(+OS><}KU3eQMc|4a0!W4&6HIY)BrPO$ae7gQIF&air4 zAelNLI)k?Q=qA(k-TiVMM!{v0Foa4e`xHkm)jDDb@41|uIebk9ep}-&UqMVKY|OFuXIcfiZ9YnXwe8; z7-AP;Wf-Wf83E`gNG99cVDDD{qHgf8&u6otl*(Y=&L4yU2Qa`Fr$a%yW&{S6{#U3}ZHNYy-XJRB0dgg#i~;M5Djg3EDj8I|Vu%Kn zUL7j^=!Z}1of9PzmVWSk?-08cYbK;GGTEs;2ouGYmkq+wfQG4rdEEFwK5x~R?gZ@+KXi+=B!$#<5bIilr!b> zyDOKWDVN78mx(Etb(G6B`70l$P?o=%_DVTJZI!_;jzWoP_ZaM`wL+7@j+(*tDg9Zo ze24ZR^?S2?Sq!ijXOx6l$vMlI?U6F(0n{@o^ZQGgp$U81cR3J~Gi%J5Ynn^2_XQjf zSWF0^KW$cmh!TV?A(2CE-{c6Uf+@6l*CtF5EZtypv&~eeW_5^x0QQ;?X*ugdc{Ej5 zV!gq>4<5bmgGcQ9TuJ`wPlox)LQCe@w9yRvUtW@9IModWBugHt1sN9$`N<)((@VRU zfEt_4H44@f+BXSlbHcReoGWd5&Zg&F#-1{Kpf*kC^2vC_suiMv%2qK>)hY@_D;%k4 zHM=5B&DvsDq^Vg)t69yq$T9mo5D%57k`eOMvsTYZtm*X_0J&m_rrGmmnmyV}_PS!7 z43RRY>r_Dh!kx`Il=8_P$8f#?q`fB8+_g;dz6G0*Xgf@KZCHWi3pMQOq3ABu% zGLA9=ZA^szYvX6Og*bu2RNq5X-wi@e@5_XstvBS*Q^?_?gdE$1920V0N67hPLXP&3 z!%WB-d6N?Bzu-Hgmgbu{$)H0mggH`;K?ot2hs=iB7dT3)RmUgGENHy91r1tUlW4V` zA(Onq$#m#d%|E>DAI`Sq@5csD?<;vA)$Q*fOEL*nyN>|v>BJnqBkAA2?e=9 z0UJ=VVRQ`>J|h4kTfXD9n)W8qt(mc8aF*eIYC+|8J{zoke?Z#mttfcekbL*H30g#0a-< zA zS!KwGLZSvn3Fw-GnezL;%o%H(OGVB@VN7k^4c>Z!)TP5!u0wK*L5%F~&;7daxSDF$ zwuDV=DbHq1z_hP|sk;9mBiu&a<<~l1Q*|roxEfZ!X(_wifKOWUrAb^^>a|BDy}WSa z$LyUOY)1n{0~x4zUj`}~8YnjgdPLND2~r1wSUivgLp+-Cs>fr=&!h3G4O8-SEaNR| yT4}eC7?bU6kz^=~B=5!|$!&|o#v(63G&@Wm1$zIX@T}1L5B~z!xJR2$d;kEs$sguX|5ic_y(eQQb}b~d)TVo%49FOs3?h+ zxuHlEMcd;!id> zel(94LA1OX|M!pIKFRSqgh(&mTskmmMs;)XU!6zU!rF63p&Xe-wEu|7JY%=6@}d_&!>U zi&ooq^Eix?(SsM>j6dGyKjZ6dH`k?pPV~L@mi{d9y}#`08U zz8OqODG`=K62FaMNS}#oPPY)^_GDlVEXr;+9&}^zs-i(!1$bL$|Bw{mD@855Xpw zg?`o52T?j$_fNxgfB5a>=>7chp59RORvR7`(q}$vA0C$X!NT91akFxpnx5{q&92Yg z^}}{eZ%pylL9otEgx-^%Y`g#BFLj8HN9)jw;_+zv9dAKra+}uIt(C zu;)ZyyB94(zv!JfO0X+8`+Gt(b;9flsq9xbn||o8rt>(7j!D80L(03)apZVd`#2?f z^nK?C%e%C`b0oWUK8urupPajN*KwI!{0PciCSBgkTp0(>a?o}*Hh1ykw1ViKkK)yc zbNxKG8ceo7{IBVY*@m{W4fUOE+W9fla{xJ#Flun(JsUy{;mPhL)^iW5Zg$h`o}39Z z2W{%U+nkw~+8vPi8VY|R?$wc~I7+JwW$%w}y;TrC>Fe>L&3Lp)pE7jT$Xa~#pMLn@ zr@`EN8AsY*!O@(roSD)s|ImI$%U;;V6T4VD1cF-C=(_z3X}Z0PR(|zY>PPph?d@!6 zr83;Nn-mZEB^^$S=Sv}0a0&OuC0TfbYaEyMh6-GgJ1+!W0$e)fiGWKNh)ZMuz9b6X zVxBK;4ej_+{*nML0WO{NM8KsthfBYO@#Fl?OHvI?{|Liiz40qDC$u*<;oKvnL$pJf zOrm6l+{_S`+Ry}X?frR#B(f_eHcO-oF~TM}6>2c0g5N~?p>{=Vu_z<^5zrAv7$Zcv zOc5-IxPV}!VGH7s@pwe@xv3nE6cgW9JVFNIQAJ`eMTn7(*{25w3vEH5EG!2UrQ9E{=0Y9L$))OYcb6xd%H}FX##2**h`%! zf||ZiH7y2G)A|=NoarmnwEmUJ>Ajk!w$ya55rUe2cWN4enzp8~f0-Gj~b>plKGss2#ZV6DxOQn#a4~5h; z&ajX?S)77;ZwA@nI5iFj%Hayr%o5gIVuIa*MluI6#SB)b)QzydB|8rpszpmB72gdT zs#Bmk#*U^>C*c@>0owcJ?5)(x}1WuIjskg%63VNa>h1{#)_*06Oa ztgxYQz<4t2c_!vHA9WG^NDNE|3 zEUPbgZaGWpBhy*^x^dPo0Q9;gK#4Av5|KWXh`tsh5(CwTDJ#28^R(7>+t5hRD%se=;me+lm|v7Nu=R z4%~ZF4!0yZcu8>}*OuboAUGgwbf{$l!C^dXNYERv6gAK=QNz64;3c)OjT#oz1_!YL zQKQ4r!XP#*MGepzW(r_`PUcksW2jwQR#thrWI|iQoVz05wS_6k>YS)cg`N6W)%alH zUWI`3`{co&E`p7|0dxNpm~!MI;bO!j6@n_!@kxGR5c%h;CeRiN5LGTh9AT(B`A(}& zj2}u=14rbNj%IsBII2JQ%LG0*ha*Z!R)fd5k}i^+5dz={wzgZ{7El96{dWiLmtM{9 z3g9{TXf#3-ZMFa-p=V^*T>;IxQOzLDY?5dSMxT&FBp1xp=)gE}1pzDqEQ*VIt~Y(o zMhzJC-lDV<*rt`5%$O19+7iY>W%amHY66ncB4!whYKCa0I2n)#kf>&|*TgzwwL;yr41lnt@ zqN$5YTfZPhJAo!F3bf{FYb&e>azy||CbHJAb+Q(5;T#D#M*_}~fO90i<8ve$z#sw` z1Q-Mu1Q>kZFo*#L0R{mE0S4a(3|1%T2)U>=OV0O&r9~~5owCxliAAs| zEMIA*fY6I7wNvpraU#qaFcYV923hWA-l!Ti1 zXrAFHEeEv_%+8T;nb8Nf^%zl;V=D05JEme5CksEZhDdMbR1Eg^QwqPo%bbEzO6dP6 z;)E*WIR&XFyw+NhA_Yfa*m(vV>Ho|VeucYE;AVk`>6oK!U?TA(KUWJ${ZeowjX%7+ zJhZwP)phvrSd&YondDHjx@~BtW_zViv%y*Be-eM~C0^D;)j~x7$D5Fh37VYr*il;I zX)99mP42iHQ5_pl$CgD`Ah;x_+z%OpL&S2^8m^I-cI4q{9j4CD+pwZgBk{%B$SF(Y0=YXu5g zq2ub~Z5XVlcX1MY)9&PjC!yum3pX9HB{!ojjBM^_8{Pe>obj2C2g>C2e_j$Y zn#aR#Ca3Z|9wv@!K9ARZJdnkMEZ(q@`3q$6j6XI5Lk`bS4)4!k`KPx$$mH!sz3QLI za|AP;%+oe>@F83=HNnV1eUo`{lHN@lWb%%NR@VqQ+I5*a*-$x3=E;f1P0yIlVr07( zt?!Yhd1W6z<=3v-zsP>!Np|85Lh4F70#S}kucVg-SG6|g5bDZo!x5GQR@2`H7pyt6s&mn07LM1Y z%V|4{@!>5wKaVROvvoyEzFvz`jV5#Tbk-b?Q%Q~K;U zj~j?9+WkTfr}K#k-L~t>Rp^R2;Ie~B(BykP_RWsINQUu6`c8b2p7TWlzPNkm1yBwI zoOBpxMa-JFBAWlt-dnRGqr<&+=Df8$&?$k^H3eZUde$95!XLwD@iO$D{N(e8;)VXROuW_S5B~>1ltqq6 G^8f&+(?i+- literal 0 HcmV?d00001 diff --git a/conferences/fosdem2024/fosdem2024_formal/test_enable.png b/conferences/fosdem2024/fosdem2024_formal/test_enable.png new file mode 100644 index 0000000000000000000000000000000000000000..5a8acfa875a207fc9d2a5b65cff0d286cf495daa GIT binary patch literal 4776 zcmYjV2RNJW*A6;Djo4eHzZx}alp3uSvu4!Z6}$E*CFnrx(HgZyRZ&&7OGvdps!=0K zQG0JugxJ2f{eS=O`p$K|$$MST`#yQjea?NKa}tj*)TX21q5*+Gba!<$?twrQVBo$I zObL9ldS==JU(|j&R)HW8eaD}RB2$!}8w6sqzN?{T`Y3;M($kW8q~-GOPJw6Fu3~Ii zqAh*Qf=g+xvNvh^Sc|aIG`ftxEq8yIh*T@B5+<^ZUu83G$J*9cHDVAVES+2uV9lCW z@TxhOCZfjjIp~GY-M-jIX;f0wj?&Z%=ct3U9{pkKt=$C|R~OeQ*acA7KzXxO>4p@j zoX5b00i?8uE5$STw_FYb1BUfAqL}^1_MV;$ytCn+-*i(*nY$TTz2fWFufXPh z`76@%dr#g)IgF1g+zBJaL709o+1$n7p2}lik{{?C*-GABE;{X^bEuv8+V^?*3|csN zdT%h8I_AriotrD~PCk*GP%?-u-m)+=Bg@Sx*ETdrN!`LBthK*x2~`k z3TSzF{OYja-6N4YE(QE1$WhcqVRPSBS2v*!Gmp@h;5sPOaamD>a_^wqt8~wU7mIfB zWfS*{6W_&4A)^`dyc;64$1+7T!ZN2b@9=RoF=GAF{rmo+OIfG)0D1oWOfpR;IWK z?Y-U!?(F_;Z@V8Y=s=;>)T-#Ex{qoW25$QH4FH{TZmX306rHNmjhH^PF6PFnt5J+z@_hY zV4@)ld2}gNWliM9d5izQU0PaNPG2oGw5y4@;Lj&yUZGa$pmO5G;~3@egORAq3@zp! z9v&%B6`!f&K%)Z1$r1x}H%Jz_aOLWlgtdRx?gTGj`Wr^c*_ z=|V_^Vy-B zi9zq?j~@Zj4ItRzQLOZLM7b_uik`robxhY&b% zXoML)QD(R`<*R;bCm~_f9d+@rRZV~M#{?{TIc2hiR0<%sRwpm zGY#S8EhsW7Qt+>RG|XMSzP82$@6k>j9vTvpxb1fTK8A2#&F2MERFGagz|>K?JT|fH zWy#3aH*dbCc3t7-A}T5xuHb4iGZ#DJt9_38m*{Gs4Gj%Kf`WH_TBD|65HPw1Eya-} zY9TUsvo#jb58$xa^`|8LTjRPUvtSOD z_p6R3vqqYFY!WYc;@-S*Ma<;oSjE1#!v?S1N4w9i43xCCy{Wb%Z)-!VWN*r1%}nY7 zmkR-37uhAQ3s|lg=puupWM%2-BHa25PewMp%56!Ja27Caxc zmE-zGFmUODg?-!C`;zuUZ(^DcTN;d?L$y>QC+21(Bhf`$iw@PKQP+g;3u|lBY&Y!3 zMi1_bjX&txuO^X5M=UUbiOEUa*^*!TJ2?$sSy@>jqhRHSYxUSz(dTSBI(~%rlPGU* zZ;i`#SL1Dzr=Qmb&b}%IWN~xD>!mmyRN6T%;ldS-FD}b&3Y{-fJ4@&C6}Va3-p?T` zCd7rG4ShU<%F|NT5~ZAjS}_Pcz2hR2$#vq8kk{dZVeYe`Mg~=e1c|F8zYtL|vD~Fq zW}I_Q-g-tVau_kL3{n!Fa^m3Nh>L8Z;2@ZiY6C%waG+$s){9L8zca_As1MMRV!O#| z&`)i)KGF?Q6hC8?&@6I3UJ3yVaVtr(oP!v*)4jlQLqb{s0XtI0|99n=Nk^V6CkMFd|<-c{&+@C&d{@yL%u7^{Y6kl zMzw)7Q#~syTl=XRAOWtU_*E;Fft`2i>g*U98NF`Z77vorS5-^s>?J0^-^ zg+XMQgW|8@@%TG@)yDyRsV@r(c!48rjx}s-Y*^K~R#`W669|&Z%D9ROkMpxr^;r7k z)Knu~UF%PgN-^`rGDEtE;QCvkbBW$Y{Y!QO2gG zK?lEQjZ3r`;cOE2twF2ze(KY{r7s=b(4k4~Cge_3;cGd0)KY{q}pxy{edXUcLs;S(+lPoz%+!$Lzt#n=-6oz)qQJU!aG9YVCNb*4`3 z3JeIa#)T{VMdgs$3GhHE3qY1U)ie0V(jhzBUC_j=g{7qg`<2yIO-)U@qnj{E$m~@( zNGgp3g!~pJytp9q0m}87Ci7xNTm6Nq>-Dl$%q4AYZO|wRj{APX7x~cvhQI0fC#-+% z&(}^Y2rW@WxhL-r%SS)bou)z2dh|hF!8W&O9~uEcpv9?LB-Mod0~5<(SE!H>?5_g@>jZe(Nx)Q$?1vaGD` zBgq;eqr#p-CDiPf7^5QP%xVWv*tc{JR#sLR3^qGE3$Pd)vZWkC%oi(~+kRB%*6&*P z>v(^Yd9vjKrgq`*8K1l#zoeueaiTdIa`~@SKs|hX_Q~X?#>S~e?>rtQN`ii&l9rua zL2|M|k@7urb5|Faz1@D5={A%_3Lk~Lpb^s2+8U7CI6K*(6$Bhy)W20TF+P4wC{{l^ zJ9Bh&EGQ@l2%=FH3T65SNFg~n^6%Myfx0K>GjXt1S>0mJ$;p|_r=+N&;vjtTczIjX z1=8p+91_;km1)SJ&8RU++HPS=}}q;jOEy3x`uCc3NYDy;B(g z9N)crw>jRVhg)P-U0pbN_^tns8Ew4fyy<#!cDyzDGJFRwWLGVupG_DVy5>*@s{c%_ z43hFwR-@T}rgP(Y@S;L&nmp&&+_zx?Ym=wLX&k0;>Yh}kSTaQqvR33$Z;dfTOy}c~KG#Id{pq7S4$KLu# zVq&7GsHlyNjS~{tV!pVv^rp1b%)(;&)8oegY5zW(VW%Drf{lbb7I&CSL2z}MFZ9D2GpQdyaKUQPqT3+pAdv?#*k5)<{vF+el`-awFEUSig- zDl5ka2Gq>TKs0bGWD@61G~}L*jVBTbH_HQc!+-HO0bB>tOVr~1LO?ShEEvrF&IDFd zS$fr*B0|#@6%|=oSvTGK>KhsijEo!_y*Oi%sR;4iw+}4E%;A46b+NOv)2PLb)e`q#W0Sp(Le;9d*iAt4Lk?9`+ftWu;(~pRV z;A){-QBh=a0uBt+vR}V`$&fCpQYSF~BQO7G^+)MV*B(h}X{2-xAQ2^v5uh-{d8MhL zp$~3=W3_PB0XF0fYDt!(kUu6hu!m?LS^2 zXw?*1)H$3Hv`@K&(HQjqc{8yqelYTDn^YHMz zc=5u0g%MM_BW5)42v_{PAg#*#=R z^6~Kr2nY-X)2J$}F_Z=b1em|GG$^C3DLa-U+S6VA=_UG&B)(WHcKOZ1_AoTL)b8;R8f`dwU!I{kuufC(vo}ZzQ;- zrKLO?MAcWPfNt1)3FW8a9w|9S&WA}FxqCQJXO2#E8n`y8In7GeK`VB}O+P8%@#KvkP5NVZ_o&Y_I`Ykjh0{)eu z3M+Bi>2;QNa&iKM-wuI5n3`r37QV-%EIfG!s#%fWZSxou1QcCG1ZxY8k?$-ETQ_QC@e2`DK9~b$$V3yp7Gzw0GoihB+koUNOfP{y~7L_m(lZ zStUJMdNJ&93NzL=3op0N@c^9ey9WT*?y~%VOI`>4AJFlnX+K)sSQL(;qg`qGe;1A} z(K8Wb4hv=a7RJTT5sD zOZ=1R&u`~gllp~C&c;heijM1vGP1IicO1B!zP`nF&EKj&Kricaxz)NB2d?B&CZOps zmODaP{vLMt>JY31FrNnp(-a2N*o2<++?kjKQDvXR4;*}0uCq*KnY_m3yeq=MiyrQL zdz=&c^E~3MwZLnT^R>rFFe=kzYeuEFr?Ri7a@dXTZc^d?a*0r=$~0RQ6F7!TL!F2N zxoa)vY<*C@+>dALDW+AjL({8Q*6oI_-SHwy5=KHjdi-dxR0y6!GDjP0ex)7HiSEL2 z`q^3ajIHLW(Q>n0C2?Z;)bA)5IaKf113NIIF)hlEuZh&YyA_knFg{N{*?E=vn)ki_ zZQJV(At0H5HKRdDM5wT=yg!20kr1Dbqh?a40SIGMD~Miskn*%rMc^l}lD4WYb)jMm ksPl5!6tw?elF!)l7!~Q=@zl40zn(yMH4Qc1!|y-)AO67>*8l(j literal 0 HcmV?d00001 -- 2.30.2