From 09834f60176dbb66e24a79eed16c0b66d3b17fd5 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Fri, 31 May 2024 16:46:15 -0500 Subject: [PATCH] Initial run for new archcomp benchmarks --- .../engine/nn/layers/ElementwiseAffineLayer.m | 12 ++- code/nnv/engine/set/Star.m | 5 ++ .../benchmarks/CartPole/README.md | 11 +++ .../benchmarks/CartPole/dynamics.m | 12 +++ .../benchmarks/CartPole/model.onnx | Bin 0 -> 19185 bytes .../ARCH-COMP2024/benchmarks/CartPole/reach.m | 66 +++++++++++++++ .../benchmarks/CartPole/specifications.txt | 14 ++++ .../ARCH-COMP2024/benchmarks/NAV/README.md | 39 +++++++++ .../ARCH-COMP2024/benchmarks/NAV/dynamics.m | 11 +++ .../benchmarks/NAV/networks/nn-nav-point.mat | Bin 0 -> 11876 bytes .../benchmarks/NAV/networks/nn-nav-point.onnx | Bin 0 -> 10601 bytes .../benchmarks/NAV/networks/nn-nav-set.mat | Bin 0 -> 11872 bytes .../benchmarks/NAV/networks/nn-nav-set.onnx | Bin 0 -> 10601 bytes .../benchmarks/NAV/reach_point.m | 75 ++++++++++++++++++ .../ARCH-COMP2024/benchmarks/NAV/reach_set.m | 75 ++++++++++++++++++ 15 files changed, 318 insertions(+), 2 deletions(-) create mode 100755 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/README.md create mode 100755 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/dynamics.m create mode 100755 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/model.onnx create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/reach.m create mode 100755 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/specifications.txt create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/README.md create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/dynamics.m create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.mat create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.onnx create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.mat create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.onnx create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m create mode 100644 code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m diff --git a/code/nnv/engine/nn/layers/ElementwiseAffineLayer.m b/code/nnv/engine/nn/layers/ElementwiseAffineLayer.m index 4e83b8c829..ff0f43853c 100644 --- a/code/nnv/engine/nn/layers/ElementwiseAffineLayer.m +++ b/code/nnv/engine/nn/layers/ElementwiseAffineLayer.m @@ -137,7 +137,7 @@ end % Offset (bias) if obj.DoOffset - image = image.affineMap(diag(ones(1,a.dim)), obj.Offset); % x + b + image = image.affineMap(diag(ones(1,image.dim)), obj.Offset); % x + b end end @@ -150,7 +150,15 @@ % @S: output ImageStar n = length(inputs); - S(n) = ImageStar; + + % Initialize output variables + if isa(inputs, "ImageStar") + S(n) = ImageStar; + else + S(n) = Star; + end + + % Begin computing reachability one set at a time if strcmp(option, 'parallel') parfor i=1:n S(i) = obj.reach_star_single_input(inputs(i)); diff --git a/code/nnv/engine/set/Star.m b/code/nnv/engine/set/Star.m index 1cf2d300ba..19e09bf9cd 100644 --- a/code/nnv/engine/set/Star.m +++ b/code/nnv/engine/set/Star.m @@ -535,8 +535,13 @@ if ~isempty(obj.state_lb) && ~isempty(obj.state_ub) B = Box(obj.state_lb, obj.state_ub); + else + if isa(obj.V, 'single') || isa(obj.C, 'single') || isa(obj.d, 'single') + obj = obj.changeVarsPrecision('double'); + end + lb = zeros(obj.dim, 1); ub = zeros(obj.dim, 1); diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/README.md b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/README.md new file mode 100755 index 0000000000..6e877a56be --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/README.md @@ -0,0 +1,11 @@ +# Proposed ARCH Benchmark - CartPole + +This benchmark is proposed for the ARCH Friendly Competition 2024. + +## Benchmark + +We consider a pendulum (pole) mounted on a movable cart (= CartPole). The cart can be moved by a controller. The carts postition x1, its velocity x2, the angle of the pole x3 (with 0, 2*pi being the upright postion) and its angular velocity x4 define the state vector of the 4-dimensional system. The system starts in a middle postition of the cart, with the pendulum in the upright position. The controllers goal is to counteract slight deviations in the starting values and balance the pendulum in the middle of the track. + +## Specifications and Dynamics + +The system dynamics can be found in ```dynamics.m```. The safe states are defined as a stable upright position, which has to be reached after 8 seconds and has to be hold for at least 2 seconds. The controllers step size is 0.02 seconds. diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/dynamics.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/dynamics.m new file mode 100755 index 0000000000..192a78fabe --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/dynamics.m @@ -0,0 +1,12 @@ +function dx = dynamics(x, f) + +% Cartpole Swingup, 4 states x and the input f (action of the controller) +% The controller takes (x(1), x(2), x(3), x(4)) as input, its output can +% be used directly. + +dx(1,1) = x(2); +dx(2,1) = 2*f; +dx(3,1) = x(4); +dx(4,1) = (0.08*0.41*(9.8*sin(x(3))-2*f*cos(x(3)))-0.0021*x(4))/0.0105; + +end \ No newline at end of file diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/model.onnx b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/model.onnx new file mode 100755 index 0000000000000000000000000000000000000000..c837ab82a96714ae4187103ccd9f37cc61d1e77a GIT binary patch literal 19185 zcmb@tc{o;4+%{^SQiezap#dRNk=X0EDN}sf2xYwh23-%CnLQ8H|6RA_{M;6!l~ z17iadi@W*4G9|(?vY{a%TP!T>*9HfB8_CFR^xe8PBGSOfVDs9bb%9YbqyP6CenGyG zijxih$`YHDGzf8y2aJg?tp!fgdbpE4#ir9a9O6G*{ zfBFCa)c=2n!{k51VPf!q3x~=70*?P^|Njk+|1{ixfn(PH0*?P^{~vJF{8u>sQ-2vn zU;n6}&=BvywZ3cqCnECy=X?Jhl!=D_r(6FC5QYEJ_Wu!#nKJ(`!zhXvn@kk{?=Sx! zFQ+II>>Cu~y)MExEKs*tO3F$~OkQ~2f8Oj1=f-T|3L*;`$_*ij} zrNC+Dq2oCx+$NL7%YQpYBZpGKe9BW2 zBbN*x>+Vy}`cv?*Uxn?x9SeJ%L@oD<9l{{h+{nJTc8NSpsl(cKE8bUb0^gohMv}AdV%gG=@$q81*lmPetv7wII8@0hdV z5W4=T#3093Dq5z-i>%DTxw3^A@FN?KHAD*EJDQ2Kx=#LwZ9_BAC`HjAdwE$M^ zN8zq*e8Pb$G`rG(k8P7N&(f8zNM1)&O1kl9{aLI!VaW$*2pF5WyD+@mhF*GI#M>3i z@HUqo(;4Y@V6?G}oxf%pc$nwo$DPyh>_Qjp|DJ#sT$;H6`)+tuaE4KEdQ9q%%d^3S z7f8sLa<=OEYH)r21cN5Xf!R9@A1(MIMuNYr z?tvHMV&Rm%GAkw44rTC1qMu>-p}nwSV=V0WzMQR9{7dKm2*W3*7UB47DZFL; zX4LMQgPno_oLPL7@B2K5x@l50_~=KDs_x*Iq#ec*xfay=SB!z8HGEb6GE5Pfja}1o zP}D7n=LL4C?>iBttlm?{^f<5HKaD;F)6$Y*Oh1)rhZ>e@Rkg<4f#w~xa+QQ3;wM4-#%c-!KoBQCIpfz(JL*1S- z;>)kig(?F^C$xYQxg&mlY0R)?W=t*T+7>M6o!W01=_SM2Ufm^t><~`k(+dj|FChyH z)pG(p*@cX`?9v9mlqY{*K0cf#J`EaaxbQSoF5Y3If%nEDyRUo}Vyj4!0$<+hXs<6^#CcM!^|zdG2V02({m~ zU*J-jEYQ$;E68S+3i|7Boj(-WcfMl6Xy#`6L4iW-UJLPiJDCX)Qv`C`#xYj$CX8-L zobZU*{BPL&PqX&Fbz zG-#d@Oxo^L;t!b%P;!jLLf;nh)wL2r;9Js9Fv#TSj)jJGi{OER5oqi5lhU

Fk{pX zXjuD-KHVS!K|1RAYJC>xzO4Yi9J~Y*ZyVyTKTqja<#^aLv4t_pSRhz2!-QGNkA^#S z3ed4QmHKLAQ_;|5I6b>Y@Ml6fi8FVDo?}lqhf*PY<8zTy+_DMBeRbvh#ZQnQ)z&CA zXon)PS{QUPni?9vq+yR+AXMcgiBV1IDQ$l^V_Xh@kBZW1wzb$Fp@!`}iO?k4z}Y4~LQHdk@!?I({L}7`aK{Z+ z@4E#p51UD@h6YKREPx>`Q9P8MLJNjh!CJX3IC0$&V>;W0HV15i&UI(V`uYL-b>UcY z+%bzwFM3Efi{{gSE*sdRxDKaQy=97L&S%QZtuT4i5v-~V1nIOkU@t#qqNP>gN17Iv zTun#+ZV|94o&_hIedy5RBUI?)7Uo}iAKfb^1xuFhA^&Fdl9N4FXdrI`$LM5iuH6Mv zl~-wAIAGXxYf^sf6#n~ai5{WLVc_~rZq@1@((uxgd~V&r9e8|_be~Iuy*Dot|D;rA zzgIYBUP(l2Id3BAbVZA#EFr#lX($OmzgS8Bnp-}9MMyCj&v?r=C8s|tSm z@~Kdg8l1iLi!fFyu(@g+jISR6GpP+|HnE8=&S;@GmW(6yhdm+6G=MbUOs41KoneSO zLgns_0qY$z1sXn!$b$6?aA1!Cb~55LHK&H~0m-x`s+nkAAA_r=K839loawX=ls<3^ zz@=XXxOEbN@X0@xlfLeVt-qg|atF935qY*SDKoew4)yQoT1M2U3m0Dsny+N0OhYbUo z&vGz-@=U%7Ozhxo%Fj51@(Nc%G_DEv@AGM)_1&e}!&40n?8cTSOB+n?Nu z1sM=KyNBdI+>I5vafAj}Qad3x_;MhX@Y?I>jp$5tOT0`f*6N{#Q8WGYLkRpjq(FUG z7neWt#B-t%%-hFj$?iYDiP2dhvT;EYnYLXHhiVex>QF9zny&;7ey1^KO&J|#k6H@a zx|t-)QYdsg3Ki?yNd{|=6UXGzn=J>Z{wp*1kkZKowz*-(NSt=QWq^AW`i9VEWOkncMolZDV{rlAJKaY+8(nZHb3DAZh$Nr$TglBQ z>%dd`I?i#5ho>tK;8d>}V7B%cF^;t(QX%`P^X<*lFJTM(@z?{!W8G+jbUOv5YfK9> z3Ma5hcu{`~sqw5P=8-aJ6ZW0F8Hr_PivFROx>R7ff;YB{XVQJoMOmGP7F5G(F^!rl z&z59N=7aKQuu9_1P+jCfo0b{F&H`K1mXu*lV!F}8G@8@Sy$9dPezM8rA{NIQf$HMV zAbFr3<~5nIXO~`qjLXO8PTuZ;JzOI!sXc_+qN!A-UJ)Z&zu~2EQ(0C}h?U9LsmZa6 zkoZ`YP1|hw^Cr8)|5afe~{j(}I1t_7T@>D!?q7KxmW8mAzYLxgWPmh#5 zq_1QLXgI$RB=^?BOc!^WYoZFX*KUOD7gq4K? z5GtMyZw;;R<_&FV5}OF_f67QyU=O5T{J>~V`A(&oVw@~R(6v(?b+S~@b(t+aS}KNH z+KY&=*fiYVDuFqwnde8V9D-Fp%INwNo8dy6Iawf*!`;7Ag7utHidSVj>D;zL*%7fCAn+w!5s`FWa0}J z;_63(<Ne8=iL3$LvS%jif)Y*%u=j*8Gf6*$*mQJRI+|%PBD=RP*@0S;aPlr@ zBLSfvD)vbj!#BeB)4)esF-DvA6bRFN@ouKP&YU_K#tTa8Da^GQg~!?_ zLzVMhl+L+EyN^c@^|RubY$AoltAcQbPYWF!YJx55uEhNFe46rDm$@xs1VeGJ=vn`V zMA@DbOddZP%oiDgY>X^^pHWX$vSlqrdn}24ZXB0U6Hn*7nnNBvA@Cw16%R9ZIJA^< z?r)~SBjsAWZ<)wk`t47<+?;V~qYQR8OF`*lPeJjLCKue=yOC@aE;rCflrj^?Um!9`J*}!UMY$J-i45Lei5B| z!wv<1m%!>PPI$+yl`NdD4E($%R9e?S-A*n=x$-vB-Rng~HqFMVccpN1a4!fF3hDgp zI6Sh*1%$%y!kkrk#7B{%YL9Cy#FGBefY`b8)tQ<2vtb(6^%|qhaTPfHDuRgvXY#$; zOE6F*33`ja(r3>{^EGQaNw20G^Kbrq$eA*lEWDG#g$9+9x2Q>5#+MOqJVn18%VJcn z_t4aZAG z-PF30NAsn=aJ`>GUxYV#=A?_y6*rJq4d0ksacQ7*yNv2@_(jeI4v;%}1$ZS~4_{24 zi+^r=6L=~P3w#~nOfFAW`CHM1zpv@&7+cb3A7@#&q+#yePd6bd`W2B_#KOH}1j-HP zgI?w&YVfL;1a?k`&q*iXWnVT_A25Q+ZM)%S`7Lghr5nt7kwawmhv0DEB+@<8&qDX0 zB5Vv!z?JX4!3<+D#8U;>l3Y+3Zo)kx3&~n_aa{W`hhEBQq}LPl@Jh*Bx`A_~K`q%d z?}Gsbo6E5Z7qe)`DgfmOvaIJiB-XXjC^s3LTMY31_erkr zkurL{u!V#tCGbaF0iDepXpBt&buO$XLy0?K(!a6vY}j2$Q%^nIdlSDT#lGp!|4@2wW!s#C7f}IsyzOWQ> zyki-mKL@DBD|yH?H$mH`WV|s)2#?6bGPUC?xswr@%+c}N$;T7QwOlcE3myDifVG4AD1?o;$Xyo0`__<_ zJ+}ov{>q|M)*r~Fo^Y-_85Zr{3#xoG)is$+R~clXx$ZJxqW4;c>__`CMMl6Yl;%5*a8Njk{B>ak^2aaHd@Ziasra zgBLz=!oKpvjSr_+Wc$c)W*vm~_R`s21$1~roZ#E_#pM3lJ+w_K5A8OLqPHTC((&fY zaoR^hjKlUYv0C$Ci#S7%y4En`Mcd&5#uDu(o=p8>1!&4~q~X__=*k==Y{Av|c2Y3B zeOHNVU!Gyex!ue{_fE@C`uAbQ^JcthU;(Fey)dt^lU@%shKWb!QI(cXEdQrZI)XpK z&Ajy_C+98Mx;PhHeSZPKtb($JgUsdBK4bk>Do_*upoIOwn}b9 zNwIEHHf9MOeR&mZ@4f=ID}Lb&S*4L&M;3PKiBhv+Efh*FCcFFAVxd(f^;i&tL2?gh z<3lG9&h;b_yGk%3e~|Qib%t@B(uJ3xh;)a`R)dL}ou| zhZl2sO?vPyppWtHQGu7oo^fpxym9QRW3X#^GaZ^^2u1RX$WehinnkB_%Ku`BY(_MF zE@ch(>N8Q-pqKnTnS;#kQ2gFdNyqG)XZhw@6}=eHY57Xjg!6x4gD?7hsY!DQcyC$= z(9lah3vBSOY8Bb@dl^2FIKb(cNkZt|L*!r6Abq|<7sT#pSx%ej58oR0(05ubG_7j} zlphqrdKDL%=u-k)`KOFSgb6G^TZkg1reyc;CzjpsCD|)s8^PcG?0Mz7<8+z!YTy>> zVB+^w2tM6OpC34Fsr<%_e$7>Y)+;mNQb!w=Z$3nxYQLtNhmFDb>klF_Fhp;xc|`wg zc}6$r1mg>j^)TR|4@dS#q2{GroT^fW!*)lR2UCY|{{?eM;gj(5;70gcv;oeHy#ehm zO&GnkkNed-iZnE^WT1PbCa2axeICuiGx;azzGL>Necc52m1k4&%k5m$ym&gO?LjtW zDPfvJ39ek#Nu#>PfbMNqe9*HAkDL0F;?-*)e)D0>HakPpx6Y^jMkjGrnk1Ez_r<*T zb1`12no6b((i;*l;9XC=KPF*$$BWTUUu<{ArRDbBy~b zF$qt0*y35v4BxEm;qGahV9&CDB&0_PZJyhK?A~-dGkQOCR0rbml8YdQ6miXM@4~aPS+YN+*t0LaTTKTI-;MZJ%>cQ6;@< ztO?$?LqVqdDJjT0jUT|&DIGhtYS&!j>r<5^*^{? ztrKLbK{W}TTtK~#^g;~h1m+)~GJlNPX~wNa?01;}DRUOUsJp^6T;T66_ZXP>;xY+V?k85wnwV}lA2r(I@ZQszbYtpS zGIs1cGQUHXjxCO*^`UCmrq#yGoE$llSGdtB&qN5C=t5R+JrpFG2OcfoxWY~z|I0+-uSKo zn>4-|^5n8;bU-@j$UdR>M>vUA!Dc-EWg$K%TUa+oA%0nXES+3X2osk4fv6vbtmNDn zxHkDPltp?#_?^$7;6IwxhzZ4_Q6^w*s!vQ?3;DMES*&F8RKD_IK0ciB7Gec+*a=!1 zy#6F{K91->>dy+C`=|zX4LK5*V*&h0yLvd9)eD0&ZP<$6m*M6}zAhQ-4;QDVqq|BH zZt}~9E4or}Md$)e2{vPw7HYG>go9Q-j`ikU+2>kXthSUd^je0(j9<>ITMmzZ#ANt@ zZDGI%Nuu=BUZ(nG4vx)uP48cRM&f<^NQ0s}?Y}t#Lo!_ii#2?>)Wez>u=OFgzVtiI zJ1_}edu^qS@ijQ8TR_6ER+Cg!YrL~d4a|=}XSD7zc-gfKr&P*gP-hW*pEr&eTK(Ya z6rYmd=u+6?H?p=@gwZXinW@%@!@M2s@Z;SEDwi!qrVMNV-^IC#*MCO6sOsp3AoHu^X^)^CS>B8Ajk-IuaG zHQZ`(FM7D4k^Xg^0V<+NU@7E33(8~v^(cw__j~P@RESwPX^w# zN#ci(VX$W1IrwdOoZk7=L7clrlX;l|I$ zbX&#`1= z;G#%&&5Fa`lNmT`Qz8r(pM-O5(lD_BXstvA>8!6J%$xCag#g&4cFh2$X#J zf@J0UkzA`ZG})s-mWi$aosY=m9$$jpu5Dz+*s+jSbeJ=h+e;_%9RjHh8enf{#%(_M zh1wkkK*e1U6|?(uv{Bs62Tk1?@%Myr@VDI@suE9;b3?Q6 zr{qZN-yI9R8~pKmw-Gncs*BcyLjAUAPFTwjwl7@)zr=LuyKAG#UxN)0p1KD!wg=2l(ZmxQL%jTbvP<4fkS8MBCJiXN8r z{^PbDvW6u6>-6v|Unuv|2fdEt5IAd)%<4<0X=U~fB~92vD3Wgfr4>h8z%!S+QMyg-63v%0~JlxLWQN^i-( zRuMFI9|JnMD@O8HX}lU>L_Fo=E&H>0+Fk#NS-kU^W!InO!22wRwH5p6ER_{_`xp`n zX)D_Lz6_dug7LV~DCkWXMLvGrPai%zh0_{~Krc-a6U)z&D|6n{MW6P;mAph0a9>II z<-5#{DXBPB!h)76zKq@*OeZcr zk}xP@jMkr(@k3!O*eXVY=9#ImAiam2D0xG!mCUDsj;F~OVn8P_l|V)UR1 z(zf5@W}f^+KB_8{>)}=4Xl#on2Rd-p1$&y#yyDbNq+~185ygVN6JaOlrstCcGera6Vb(h)n{2Jt4 zI0ug7^YGoCU)VNk9Zo!~$gh;Xh$|Fpu-dy8ms~i6d6WBKfkh!vYxzthG?ua(?!LpI zn;&4U+Z))fs?SRtGvzEN(F2 zja{SY>o9pREu6*=eLDnl2{G_=_!&KD_Er!#u7(N8Z|7v~WoaWn0kfoM!6%WC?}BY5 zwKYO`W62tjd9Q)Ln(73}mjUu$&xFWte~HkBV|2>?Jyh>cCAzEyDpQif-TAzNcCFFE zJzaey#xVyr&@O5gaU2ev7J*yK%jrzRDR@U}3heXtr61oMf%D^bk}qN65K?3hX}3es zdF(pO5z?ST0x6s}(GeWZ1mX1R8Z@SJfJf?$bR2A{Z*bi=)~&X7X`j{M`u;%kP1~{dvTM86;Mh zCGeQpC~OOkWi(Rv5HBAuyqnxjFL5)VukN~KT}&YjnQl())5REqFBuRBUTpN!#RH=*lsI&-vd97gzQVnR>`w_;Q?jho^^bw_w!*3XjUEL;nb^Ou2O z%`cGZ4<_$l`$5Y46(e;DJv3|z!n;4UKx0P%?4Rk1Mn09OE*V2QW-P}~P07r5yE@qD zl0<99pQ87k>Y&cs1*lcwLa%L0r`d1T!h`5IM*L_g_@?_1r~8Y*@8mSbDKQ>{r(}?T zy^HXXMgi>+b0opPy67=_6vHc>;pm;oG*)C8+5c-gA6dN$rwysFw-gUxVMo?T%@Np7 z%boaspRSSGdjgK>(ZIQbci>7LgS}Bf>}+>kEUC&SH>QcOTJ;r}=CcfcjuU7752>&t z2_wiTsIp@8A6%O*2?sRhLSkD2{CyjbF8MD>Vu~@apJn)EU3UO8MfpUTk-GKO9pKh% z&3>6tMiPxpc=!D;NyQiq-g&qP+#71)#I4I15#kkXQ=)z@Ge7 z=&jmL)IRSe#oP4Rg?DZf&)pN*vha9t-gFdj?QLjjWZ2EW6xi7wN8t1LbZ*FLH)IVg zMD1b^EQ~OMgjIU*=fr3jE&Z2#l5r!~UzLHc#7Sx+H;)>)r@(0OM&?4W7x%?wFT);@ z##=B7vhDP_7yA!zIRy>W`jZO$yUf#9hucu=um~hvI0@qELbxtN2dl*?WS{CFE1Is7 zM(;u#l_5tzmY#&}&1Z3i+*r(c`kP$bz6W+>*kY86BB*)FU|Mq!-EJ)k(@z@1k>3on zK1UrRRWGB2yBI3(d_fQCucMJuTS;2&auBgHz=kk!YE?Rwd{=nRJ^yf@cE(+$*<;#B z(DKhTGEx#JR?P(OwGB-2*gm>(TOy9TQHk#z`l-5}A*1dU58dxHVZbI0`%DDfg5f;S zjMl*i!qf5HGiQ{Q*oe~-of*%t4d@u00&{&bxspQxkmUP;UWid8I|me~Yc67Gm_JHL zT9dBN$LX^-wNN?Nfbc#Gsp&K`u5NP;!`}#mc-dyM{jNQ%a`C}ISPfHJ>q(OS5%Ts` z4e_@>LOdQD!C&(gp!TbuzS)uw&qWT=hWKg-+GI@@jqqmc1ot^@#bq?pDfj%1hAZ6V zG1G9ZlNdh7~xV5vjUGWe*I)K7OF2}=lTF#7Sqev zubTp1`I+q2UkAArTo1jnM4tWC6odOin((Q-Je#rZ4j5X@WW_J@kh5kc+bsPUs;~OM zcx_eo$KWfJUvL%Ftoo?Qpu)ERxUsd=Tm`r-R&KWwy=k2$tM;;KkiH!L8L@ zct*ks9O9ZuhnEBID)9i6dcx6vMFhO|DI~uY6=)m2B}d~-=&z^!IJ7vCcs?qIhk-UY zc-Mjbr6S6N2I5fgl zXwaC^lW^^y`y^Aqa*5QPxQ)bX@2+kpdit;Ft+_2^fl?s-JvRxz6HzvJj|=ubUqpm7 zv*@`WlAwBIFFmZ6OuCC?@XULEGV#?bE=J!QLmIDhaDNueX{jZ)n&;@a5&kT{$QI*| zi;=^9>iAA74V8ylaLN7aDWl^$NVAg=$4(mb6*c!XyllM{!H+qDS7_TpCJUberHH}*&XtM>O;(AAsC}QNZYK6$<_FAI&=u-%QlB3PkWtup4{fo!Ezvt-eYg16`fPi|4=|G;R7@pr9L3Zeug2{0aFwK(2 z>&d|ibRXT7sV?AGRemVQ0Ae8sJs*TQzo#~Yc*))Bh4U)t;eAd5N?4|lW zn0k9Dzdu!xomDfDHS}yp&GrX)J0_ENw3@@K>=ow&lnr^_ssndcTk^rXRanOhbFjsu zk{C7k}koR$n+9 z?P1QZxPO5bU6Xf~6oKrcRH{T1+X7GmQkXrNT&52BSgkq-Ia0!95Et~DtK z9-iKegM#JIey)~$k+C3aGPaZOoJ!7F(UGE#3-kR`28vG^vDNl1baLuhWY3Pn?h6X= zQtKvJGA@f*U%1oK=~Nlnvq)$}-;mBUs*1ww(btJ~XA}IgUjmE9-=WbX8YVk_J$~zp zr!Rw^(!f=JNz&X>%-XOAtmhUmvoj2#>YXGv)ijCByd6nA71qFYJp~LnC<4D0YQW>( z7H&-4B$%B#1NQAKLbh1~p8IS^$Qwt%Vz_=fH~Wk4)!F0aYB8L8CJk(DU|5uvq9H`P|GCb;V`yv+gU6Ydy|*T^7ZY z^B!`Z+fQSHT{hB5KZxEAUr1Y4Hli6W=U!Uv;2vn!;IdU6xI5e$tnJmo3}Bsp%?J$w(Er^T%oJr%zT+tLsuqxskIG>E<7o8qsDKNh z<>Y1SX87x#2fw1!;N&j_a&+=Mu;LwPWb|ja>MFxc9KDaW%sLH2jTec<=&>OBw2#_J zhGC3L6LHIa&up4C3s6O9jtP~@yJZ2CR}k6$z++4qI{T^A@`bhrW2#1g6R zKMk@Z_$JNux_|*5qj2z~fa4MsaoMH{y5YeXyr$s`fl5kLJ+71n^xBf-jEk`Gmj>Lt zF&kdfi9~rsOLVtzHJp5~8RyK1wAnf z@+f=_jzbhu<|U~+9V6} zSH_apWj4fo$d74#wG1amNz)ZddC-|F3$N$AB#Tb2KxIE^ST)8Tb|}`6S)0*vR8%ef z>eof+&uf_bVI+63oQfek=Hav9Y%Z`*2yD01Vu5uk2DKRAno&vU;x(dEu~C9-^Q)Zx zs~^m0{T>?Kt_VlHOw5pb#_N%~IXR4w6StU4^72-8J zY22d|4hi>;g7BDpV!1>X^k&{9(PQt^ZF9RYI6z3S==_LYCp8qfuEpT6ER%lv@Qy^> zk%v2*50m(xt}s1s9}GX5fOOfE5uIQsHaOHl;+W+?7YCCZ*Ami{TSU)D-Y1trZ`1J1 zH{{J@b*y2-M)An(6$g{gbbIskUu(S=@$Jk)^?n`8Cj5mHTpM%HCWpQ3o z5}F3RrM%l3TxcUp^hM6niGy=6f6qwGRW%=j&3)J!L$ntm~=B)n7exhJU$nM=Ws-7J8>;h8o~dg!91+)$sigy zi6jl|W5(Mrzzs%w@bEo73%^&J;haw?SdZ*@PiJcRs=5YJbsHFW<{Q1Gxsn!-_`2;W zd6rWPa>%M$CkXUEO+y-^(L|<}Rw-Yj*DU|gg3xEw`D!O(Tn>5a`$N$uzdPHknpA4l7TbiOzAOHCr6+-qMYXZ?c&1qdr87WIqccK5MOUUNGwkU;OrY& z;F~K;X$6+47a+`d4GZ zHeuR6@fnP%KR6PL4l!Y6$}qD?8#}AgsaWD(-2Le*x6f4#zHJePpX)1_HwW#Z?VS?_ zT30|gc}!e;g`n-b7xh)Y!twiRVRmByNF@lEtD1iy*Ib&YPaUz#!e*!?uz?@#PQb5D z!tVOjc%!w3vn^{TSCvIaxQ2SVQcM(ORH&nVGTk9K2by&5<5rzGl2 z4G^6TAE@K{-6YIzw;)L70CVn5Esc&ni&{6_=srU|w6L|o;z1qA-~Ec%RO(Sx{}CPH zv3rdDlnRLMbSHlt-cqZNot*6VAtKTcjt72zBbqb&Y52T6GU?k}`n0eD&F{Qq4lEsH zROXvOm6-&8@yZtDmpXGVyhHI&R}tZ(j8J268!Ru}L*oDZEeEke6YQ&jcIcMi?d6a)6IQc(3%V^mfwS;#CO2o8VxvZI=~c5mf$J{J4`ZV zq0dji>8Y5acJF1XHvK$3a4Q}Y&FV<%Xr9K&Rik=@K7ZyD0kP@^GB~Ax>&PF`9=|sy zFPds`)OA<Hi}?E`gF*kZS>66 za@x{J>0F5*n0#_Sqi{Y9_v}K-q%MK$p)&Yy+jf)+VY!?CzH=|{caf?m;+TFW4~0%z zVdL$QTs?F#?Dvv`*oPHxF0~BVLxie+x<}ObcoMKW40ewAX7SyM%+trS@P_kSkQ$x~ z)yEPkdnOSp*M-64mOT8tsB5Giz6*?{FVS~`QLtd>1XG{?geoMs(}~lIaDV+uI&qsX zX8zs_0<(N_cex*(s5t-*_ZAZAtaqfkeLTvC2Qmul>qy0NbHu!ISoM{KpJL(oTQ-=E zE0;#zq>}t?jlfryOlgvUxT;p~aeMj`&C+FNCS8{ym``FPW z=S_me?I>fM0UL zH=CDJiNiaY%;z`I=3_12 z8rBF8hZ(-jE`{$fTFoxEeFNYWGQ(J$7rku_&grRqdOrsV)!jQq~J z?nr0fJ@;Zu+Vk1$KWo`;i{otOgLS;$%4S}Nj;Bfo-p~%2I2xEcvi4zh^waTYf^7L~ zw6bt7jmDW^6r_O5zn&&>9gTt}@qgswd>gdeRAu>aR~(GZQoy)|9ptuFHBI^9MS|kg zNq?sley<)YIQx1U&UF3A{3$YpQi)7le^Q7j2tF_?Q@Y9g^Pa#h7>CoE<>gfOWZ4|Vd_rO;E6KWmT#iu0$qsy*p+PKE`8G>D`VxckoTd{Ukb6XQAN`pqje{nQyfSo!-Ub6{lpnX?Pn(i)G{fzWdDS zZTrdm@@85tVg))iSGcXtV=!`2Dv*!rFi>2CR~qA?Gx-G35phFA`V*9v zxyMbnABXl&bJ2K73a&e@PSO>(pkK^fP@j{>EZ$G)L)SFaeZ7L%CVVHon-y@i^#rh2 z_ovYjuJ}khk_OjH!LZ^;9e3Gkbn%Nou?wfs{=_?Kmo!Y2HXSFj)pzJ*z7hTmdcwL^ zArRNSNiXO2(jJFpXi_~3`OtPI#-7ES4?2m`cYD}#^CqPy_QU(Gc@UdY0}jJynWsTZ z;qpHj%R2QV%-yZSOy=z-8X4YA-=3y4ExnS&O`QjoZL_Jx!U*y*iG>&6&Qb^QT-v61 z3BAw%pnY2>(GK6cMD}{QU{hf>y@3$^BA?x0c=y#=S@Gd=#p2nNG9h)mio}>;QE<^bDE0j*4E8y1K zc^J(GavQUn1p$tRz*rk_@@ZS);LbuiV_1#u()mkEipP@G?*1g<%WJ~&LF9a004RUh zz)ej&$oQO`%iJF8i-J>5czo3g!I<`=uxr9hazLAah+a4GZ8*cI@)^uNOEu{I=?>+> zgTyU(H>R94g9*->I4SoPm+LIR)k`1Iid8en1?i=z73Ip*xoDG@o3+qx^cFar+)371 zD5Jy~2{QXu8{Iy}8m-3}BZLRhz(Wyqe255~U^+l@n+lxn|G_A1noM&aIK!t5cQ9FF zK&G0#WNd#GWNTWn zZW(>BcY-vZGPXz%cEk?O+Ro))9Q9(!uSNXNe+x0Aem)brXd$@$j)5QJy!mUQvYblY z8xnke51x28NE~i7!|ZYyexr{PuXlG2%2ZG1S&^rhbWRky(jTID-vZu!cmd3F?;g=i z+Jah`8GFrDk>6h>!J5Y(hOU4xs>W;a{_|c6mPR~-33+NX``B7&ACr$aX8$4Y_s?c^ z=qdcUG>5VKR=^BN$YQV3J=*nb9SY{UkWqZ zH$YnBVa^03lfr#y%NjYlblXgPyIGlA)j=>eqK!ORlt^o5XyGWSawcV*2R*dy9-2Om zqE!(SvBBPzeDjt?u?-&F--D}2!#yoDl-9znX+VlL?WPmdVz~9G`=EQ|Okv2~Vp>(z zfByW07{+aH0gu1-;f{<*c7^>ehz*e9D{U9C&I5<|WyTfktvO5a=i?OI)S^sm>sp8Z`ZW$Kz~;&;=+@9vY%AOk2WuzMk%pgOht4QE>P`_H?G z#l7h;#VZFQV*Wy|4`ZphoZq>v9_3$+sO z)rm0m+lNHez7;t42)eLb0&yBvsC1l=wr$9vqarbxJP-|r!!>O9XdKLllF-DXb&&7* z4yALG;OsUroPDiD$~BZQSacjkj>gbr{+A=VcRUqkiHY&s4qRaRiT6F+Mvp6sagOj9 zP^B&bCKq08%0^dJcZjR$7MflwfgkrRgx@PH<*7EOsB2h0vRIP>ufil`<7Q2W=s!Y+ z7S4m_E^kD?c7_N=7s^fI*#i81_^^8zYD^y_g@aO5b2=a55~axNLmised z5E+n$PUc#`X}3QlSud_4i{L*|y8L_6|8f$%ugXB~Ik8AnP>ody5fIoh2i8FxFs?3$r^gW&JLw|h7m0s3(kFqNMCOnc<;rK@^L-)t!)amIuMPxwY;Y*-;{<1mXRa7 zH&b*m4ysjmaD@6Hm>p)0e&*-Lm8>DEe36N)+$HFnxh1q@N-?`fe0}tymyy$g`UUky-fOEIgY;VPo=7! z4d^$MEX;ZlB<@@Z(#F%M;qoooZ6kznt4u&F5uvPy8C1i@4-GHVLKRO}k{g9$u-1q~ zs!%a56s1Avfkbc|cap@MKrnb<4PAX^ImpZSzU94&=^xuly-l8={H~RFmc9~~SrkC# z++FChtd6bE4WRnZy`j4!jPCrR4wUFK4D=R~)Bt{8`yiGT%zGr+d#V7D01>Hsmj*ea zS+LDO4{I?;$e6qZH5_k44FmqX|7auGHzNtYG;>6arHBUYUqobnmSDf@7`b9SFKC z`J#V@t+J~nrNtfiVUvV*>sr%mJECaFCjgJJBzRok0(ni_(Oxs`q@6yW`o6dZ_(44h zUv-IHV}F*!tT{>iykbdxz)@J7A)?V~$EdNB5BX4&Pjp^grIH4qs|!yc-^5#FB={Qb z3;c-NiYnN@a})l{$KkmNy(M+rr$suf?0zXuGq+~#8$UA{z8P$^=|uFq$5)I=PZgtY z(k+ken}`=&oW=NBdP|zC&avI*i*b}hh+U^*+%j6p8RtL2hRSZIOAlo1&Y>pmQ?WL8 zcfmC_&sKp86MkmO`-LQsX0YO?srV0vC9JI~p407ZVa0x8e0ii%a^bh5>;ky}b4#=E zlqF_ZsF;9aEZewgU2o*gvlp`!qe*hLdMVp;A`$E6YOo2*=HZJj8C_b$@_?B>Vs=HpC2RHmFlxWuN(568HDHpk-eVbQyYnMm=HWt|1`A1jPz87n zzhnm{KR^XOm{?>~)U|p@Sg-pjTt 8.0 s +x1, x3, x4 should be in [-0.001, 0.001] diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/README.md b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/README.md new file mode 100644 index 0000000000..ce27712094 --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/README.md @@ -0,0 +1,39 @@ + +# NAV Benchmark + +## Property: +The control goal is to navigate a robot to a goal region while avoiding an obstacle. +Time horizon: `t = 6s`. Control period: `0.2s`. + +Initial states: + + x1 = [2.9, 3.1] + x2 = [2.9, 3.1] + x3 = [0, 0] + x4 = [0, 0] + +Dynamic system: [dynamics.m](./dynamics.m) + +Goal region ( t=6 ): + + x1 = [-0.5, 0.5] + x2 = [-0.5, 0.5] + x3 = [-Inf, Inf] + x4 = [-Inf, Inf] + +Obstacle ( always ): + + x1 = [1, 2] + x2 = [1, 2] + x3 = [-Inf, Inf] + x4 = [-Inf, Inf] + +## Networks: + +We provide two networks: +- The first network is trained with standard (point-based) reinforcement learning: `nn-nav-point.onnx` +- The second network is trained set-based to improve its verifiable robustness by integrating reachability analysis into the training process: `nn-nav-set.onnx` + +Reference set-based training: https://arxiv.org/abs/2401.14961 + + diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/dynamics.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/dynamics.m new file mode 100644 index 0000000000..632c28d9ff --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/dynamics.m @@ -0,0 +1,11 @@ +function dx = dynamics(x,u) + +dx = [ + x(3)*cos(x(4)); + x(3)*sin(x(4)); + u(1); + u(2) +]; + +end + diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.mat b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.mat new file mode 100644 index 0000000000000000000000000000000000000000..04e1915a0912401bf650dbf6b9c88564c64a840e GIT binary patch literal 11876 zcma)?X*3j$|NTQq_U!wXgzS|t$R34gkuZ}avM<@kj8a)5q)4`qkUa?*#=bMzw=rYi z8D=wP{e8X<{?GsSoO{lFbf3M?x#xA>wkG%Qn3&35Q`eNWHMy_${Dq(A71_If?k}GQ zhWP8t-ZgWww!41yimX|Pr~6CKXR?6-`m*=E!(?sUqhw{ZWwkW*wRH8hG-b6lwXe$l zf9lNt6O*+q?|<1q^~{;byqC@#kL-6&plYQlqKo!$xx;}hHRq?rt~&Fxe%3>cZ>!`o zN>wuye<|$=$=}YnR$O_DBg00%=9g_^j;1qZ2X_o$Y(znH>=An?iu#t}R_NGi9~dnLZz0l!81L?RZ^$=j|6I+m=`v zbhnk#3T^gV=A)*`=e+AinwLdF;Fx!qh2sxRM}~V_=2a)Z?fc1>(qyyO_cLGNY$q^J zMu=^%F&}h3)~i1cVj?=jC;-$6@^gHY97ov^koQjSWn-h{P#L@tk0A`Fmv~xPtgZPK z*?cz21CeB{*25uR}+xAbOB^ZHd7oaQ4!L^$6NCrUbqCtzB|3*!u9 zB;yN8zuc?Kz1kFT{lHN{01HQv&S34%rLY@~J-Z2s-FwCUi1BZYf4_BZO?vZ0Jctcb zrY{-^^TR7-Hhq#+neq}HJU+p< z=g^u4=M2Q$4YZRME$h;P$5^8$E+U5K0+G_&Zj`TeQn>TR#4gH0XGc-V+elH8F~F2fGn zGjhkPR_f>;LA>AlidI{Cpc?EcXrbBDRI_wTmC#FkZZ3!3HDrHzRh84TEdw{yLkgBEu_fkU1@p zE%IM8-VmTh564EO$k7!;L{g7YXUPgkewZ0jxzG6)G)z$P0C{Av;?;#xW{zWr0IMN_ z_LZiA9MmC0^eR{j;H6Yh>(m1{z}OzKYeilZ=F(#2h|mU;V|#C|2l|Bl{_ z)g<(zf*9}U`y_U+&}|D1HB-qcQ%O->4;H@u(yGpcpn?mWt)k)eyjmbFy?0w1935qk zwWXr}g-&KxWIOhCTM_uJzW0kY6(zJ-)dP19`v4_p&p5sF)!MJMicu)w%)EBwa4xaJxIfElgZ1nWfmvfKbTNgJ5h}Egm{4+8EqSUc<|LP!QoGD(4rv{oB0YFeD>E8 za9(xjd7-*Y?`i!rxcw0Rh*HzfWS8hGTv$~?PN9v#s^p4O#_5Y&q04uzvHg&Rkv|Ac z#-!hz^VJqkSY@oua+7?;^?k*d1#R`m3EBlw51tgH7(mXTYr}72&ZA@*5hz)XkOW4z z#53x>UlH;2Pg9#W&?IqIaPq0*kw?j+cW$38##4qXihBBuXRLzK;@#^qcV*bXXo@yU^sPcbiEZ7Vk^q}a8n#GnU7<$vm*CkEy4Kd6bd*~?{Gnhc zcrPoQXUnhlEbUhJ*A<{o>cRVZ#+Y}H*o!gQ<$I^DJ>Z3KS#0*pAbF~TwfC*IMf01y zAD{BTe%6+xv#)cU$d=s)C`fGq?|pEGTUXn!#RMp?#(!z%jk;+ZA{Y!(+2MrWM~_*! z>K1Qmg96^ak?tj*Th%4|U!G}s_#C-|)j--GRA!*L_RqBXw!i9tYws)KixIbefY=cp zV8dlz>TpAZCY0OH1YkE}2G;Ud*}V9%t{~F) zN<^&jf^0(c6Gd$8%O@bw!>wC@o%T>ZrH!pu&1LHk_`&9k)=N}79)t<-^VnOYLV-qS z;50!_G&Ljtl~t+j?K$fnwO+$Uhu}O$nH1IZ!hA=mt1&N0J9=)iea9ostUc})^7eV8 z6%7{I3)A)H#48JJA90peszqjrIwk~nVh#H*8uTbH`EeYn_q%d_kIH5z+^fNRt2(Nnr` zGk_*BGCoZ#w^kl?&Lzs|u%Z9`u^Qw2-dF3jL3Y&q)Aoh2tf-fXpN)y1-*8TG9W= zX|UHeJ^PKtfy^a5mXm^{08)t|E32LR)0}cmX(O;!Kab zCsMJ8b5J!*2EXRTZkXtBz5HZq-r--a!wo6GUFd1H-KoCZ2NgqvCi>ZLC1df%^SEBJ z+f=`T5FsPLIfsB-y2ZWcwl?N|73LhV?T})hTjj2MaN@Sk>5;1d9Qg5BEJD(se>P=W z{phyZI1`~jYgY}M^);7;I#e>ll3-Ir>&_uMeVaXHIm;jPvb3F3noGI<98teUoN>H2eOvE`c5m zx^zre+GzH$Y;7)$L*K#_FGE94!<5RiFV4*S2AbMic34aW`!E{nDv_}l@D+^!f-oiP z@mY_m4bGUvt+Dci#@Gj)#up2*u%?YWb0Ft&;V63@F+?QpyZnBo26`Aa*%rx3%zh17 zcaR`uTtMc-n%C8+ZfW9Uu)2$1f&q=3yC3%W5j6D7CC# zH3(^5=#+%TP2T8F#(QiC!19Cl5hevfMEaan?cA1Fe?6rh^R^53Z#XfPy)NLut>;=) z#ASs4I0x)u3$T!GSg*Z)KP&ZY`^HOqq>D|VWr4?M*1Y60k2gH95l@*?a$rv;kQwEE zKPbU1<(Q|g5=+(J6<%9%#G;|t0T=&Reo*QqZK?&={F~F=5P=0~7(2@zxT#)xApEA$ z!`-%ynDGT}(#Ix<1z^&M#8T_X2y9Nnx9gpfO026gr9gbO^G4f?Nkt;x?CaqI*o68v zvDJi+xuT4@Ype{TT?`s#zu7lv>LGEB5rg-7Jf$_nXF*C^CX7rj1!&6Xy}i@_m#TZiKFyiU@N!#Iz51a`T2#lyG%^9)qdzplA1mko4~W-$ zLx}7vMLr@mIS?-HSA(NCT9f^RaMQ1E4}cuU!)A1>AH4GF?tDY5$Q0s-;~x|x1gGUL zCi%ke5cftR;+=d5rWLc>ZX->s59)v%F1HJEOPNG|^|O*v4-J!ujPA30zdcn&%T5p% z8Rxj3$y`Fk$F784yF05=x%pAaX^D;Dko(dUIbFFC53kr@#1)EnyQTAf>M7gDxhemU zNy$%*k+>F^!5}9zq%|t%9hYsI<9ny6vf%8znr>k9Qt!TRIP@m05H{RC&8)j@Wix8p zR%ZF7La6r$fUgneSBCz0?4w9#Vr=jLed&b|&IKtM>c>p6MY;#zB z^!~ufpE!c!M&ToLTji-4kJXV}Fq)T;@BSbu?2fJrw#T>a)osI2?x@YT{p;>D6~2V& zS`(xBuB2u(I4O8BlTyJ{11MV*ov~-C&hS#aCK5djtxqW}^y}4g#5^UVFG&=LAX$l- zrp7(|fuB2|(+^+aLC49lb)^Z3m49cgR%lcAj|@h=Z5ab|=Yc=I{?I|de7dOP5vr?| zu18E!W@EQJjjIIyjP z1|Ia27K}In_kQmVQ}DrNhH|ZEOAhZoN4dv3sD7nBb5-8G;OlcoK$cp=Ue-!OPiHSw6#*9)ha+qI@sEU+1Q~A zSENyb_FlHcfcf_}3V>C&OUg7EwS;)2Pb>eTCL%)NK;$?7sZ|VV?c{5-+X!gP#ydpxFvYq6ao1SQ|`t#qR=rkJkN z%X{B!QU_FHVm$yTY7X@Z?aJDKHRp^>A^Bfm&3;@vfwj8>-CM9YFlhr34tjbupTqUC zR84if(S&XsymBmz6m#pl5Mhd>Ns*UEQE8Xwgvo-rhEI6S*1OT4ev6IdzAx^4pAv0c z&sh2v#B=z$5PJblfw+S%>m`86UFZ9FbKqr{O)y0wjklR8m8}bPHH5+;hy}xAzdJhL zU1sSLC;3_pwKt};_GeO5?9(U4)vjYt_RBmet4I@$e}${p3t}^=MOB6E?avq+n>Vpv z!pG`r9s4=J)(F^5xV1w@EuoaZ86HAqCBf)JpWwJsLo?*Gt%0fZ^r|8mvCwWg;6%o? zm>su)+>V$$v0TeGdo4o2*0It|@Npuf82ZTm#(6-GE~`dn!kC3r)&0U0igm=LqX^ka zNO@o?*?HO71}`)-J0D&Z(~f_F#`K-XCUw_-^Xet&K+(TxnY0Amd}l_rD_46hfZWv{ zJ@xOwjX-DH&BD5KN0B?X!j9ypRXC3C6AJ8&t{z?>%;|E$8_IKvr?uQVQEQb{si-uc zJ(qu8a(AAx!YIDjC55q&Uqj8B7l6j%qv#$ktH>2K+}&i1=>oySmt^9|ge`D{Fz;Gq zXnzTh3Sy>T=6N<=FdW-q@Eww=yFv%XxbwD@CWDoL^O*^HE%yQyE+kQ`SvmqOD14;1 zm%ZaL2WwhLX@`Ci;RBVW8BSZe-$Kv+uUvs-dXDSGekCIx}h+oD`K3Dua5T{_`6 z6`h|13-mA`{ yAFxUr?)>SOKo z&yJz>kP!l4K&x%ZWMC0N=GfeOpIHyW2s>%2FBG}Q!e|x)vyNNsgodEN)3l@ec?JU! zyqj*@5iAIx*IF>}IYKZ`$KQzf0I{(OUCRh%+dL@9Oghm@(*!kJyjcVGrpYX~wFC5uK?u~MuvM}v$Ff3gzqse0wTF_QY)5rC~GIMt_l z#cYG@3e#dYjAu-t#pP1yMS*S0hjLWolN;;*t|-*3Ny{y1tWx8C>HI4UoDxF%TE=cWSA<`n zm)-wj!bmQtSc54>aeOhpzNIpzOc76IG^k^Z3ak!IKv5!c@b#BFn(IwQW` zg;q^eZt&`@S9gjVcaDGw_m)JCp4}3T-@I#U&|yeoii+tk?v6M zYeWAE9wWNsz)s9|wSqOr#wR5V``RDqu4)EWq0ROUFf`5-p6BUiX;(_&c46kOdmxAv z_@{sN8h!U5Khf81@D%`ivg$ZuZ?_3)`-tk4apmo(*{zf9X>-Nv@kCc;90}qQQki); za$6B{P|tG*f0VgT{{8$T(gA#s;12Cpr(GoKYH0M(5L-ga^Dp1O3f%=m-czPkyZ|pn z@hQRkpWhOIW-s~&g|_Nyyzhu27=L-O`Fr+yKNC*fAt57b`?+n3=k`K!;az{-0+WNr zc2&r@W5;SSjktN`1@mgd4|`A~LDLaWH+7#!70`4TgGj3fzB zJ8ndsrzD~{M1trQ;T=xX8Y=um?mDIR`|TEho%mt(HDuAHSxw@YrRxCPe1*P?p?3%k zYO|3P^oLK1yeb56HpDy2Ik2OihXWq&vAkQ5G(s=neZ5x@u*q+^(z}o|Z&r!B+0LM~ z6V&KT;6@_CnO3KRY!_2vM%}E8kBnI)?_Y3Y!I-DDbp$sKFq5Zp+YHkv6&(LEi9XCn z)_TvGPTzX4V$;4Z2%UU#)Rj+r;q?yCiF0Rw7fLTthtDCt#ah0!l2pz#T5FpMRlz+( zy_ZZ;_$u`lV4>I{=Sec%zW0D~4=TWT26#YuLoHt#dWM9Azm_DA(T|{``;mfuU1s!0 zPMXZkm3lBpA}yghPTHdD@p3%s#if0vQCoxexLqDZ2`%RBGA%=(Cj($Vpse?t?&?wYX2{e>w- z`&;kL02R6?a?*HAqx2KVwBka^=1a1NEBhupMPi_&uV7ZU4yCQiM%iQx!K47J$KTwp zn@CUKZeP$MO0qzO?1Vc!>cby0@6Vvm-cU=+AB&uO6vJ+*0oryOzH(D~qJ%3?K}s|( zW|%iYp;q+;i|Cd>*-gyCM~=DK#P`f&xAK?Ly}lo?fP-p%YJiV0+qYV0s2^~jarBM{ zOM1^)#wIT@i-aYxOF!DW#tJEl#N@HWZZzHc(f&TJ$uXG)hxyDURbnN%I!5vpUVTLM z5~jLYt1{bpSD!GW3Bzg2O=MGhY$fY)&yKk9WKAO~&iFE6I43*X^JbyE_lPOXz9xw@ zwO(>0Q(|I8YRLO16=gU7j}KrHWjw(f{gZ7Al$5WqW}Cr#WVafV7{XztN~&N{OJAxe9;)lN_8~z z7!-lzm{Ztlu5U+_S~LfKMC;@=X-UDRyv0qZwgZ;1ingXzBb#jF^z7f+LL>0xHLWV> z1xw`IlRpm`pR&Mgm zMogO<2@#C`8&_sCu>;2e0{a!LUR}Tt36|*lZind+XAhOeB8<6=9W!;=S7Ki)2Jfxw z&pG)?^BPK6yUCRm@UhT*A|$${pOQyS2lgf<=@p|iK~CBj@Rfd-w+t&ald_NwosQu~ zPWbd&KB3RsC+ZTyCHfk}6shPS6gQGDkl4vcRa5;X3V)R-q6XlKEI$nHjw=3dahg*o z2B&Uc4G`5EOwyju7UGP{Q2~obsH;qXTdvz|hPz7|@r7c%@`EA?JjGHG{EVKs-VT0; zR_!xuM6M~OUsjU%pWlC74>2F=kQ@ zuCJ!bhL8ZRN_u)K;$?GwEQ4E$`NyWST3%W0g7)&e^fm*NavNO~P(4x{usd9S12AwG z*Iwxh{|c{$f|SZ%9RDh(o?W536wWb4%FpJQ7Q}cOqkOMBm1E*n6Gf7|5*G~vSY`!V zuTFth_tyoQ;h3;>mX>loY%}Vw`YDoWPjjvx&h#J78*-K|B{AY4aY=E&El~Ez@{`bAXy!oo#n9WE2{-N6-3|~s%PoE70?Un9 z)YBvB#sm3H+Kx2VilT#A$yT|TW> z6?30WQrnIa@1)!)-fbK<>EGcWTgbbIiO=5ARW_6>L|y zueUrL@`WK>m|^4b2XkIu7SA<*S99+A+rJXH3Sx0tjXAus*^gMtQF=aATwo(^T1&Gi&6K2?_KwkF(smQFbd&tLmUUv$hXDQyZ%TVkZEzxT} zTo(V$8EFRdF@UFMv)LPPL%-ZR*Ls-=H*Ymy@K(QX`}8Z|xs^Ii*-tB2eCl4d=SQu+gL5=kWy~v#ZA6u+3%;$o~K-<>~JvRm z0`AR#oT!6a8tZ&zs<|Qb+0RPeaH%7wHk9Rn+LA4{FET(psusb5?W(zye*2fTQf-~9 z4J3SAXe*gEcH}bJzzpuF`;MH>UpP@KO8+Kfr)bw-U?yYs6`Dn>ZVMc=$|kaCXuk%oK@E-0Qj#Bd*qMO#YF?j+ zyCWVxfiIWbux~Fs*LE4xJ+DMz6BVwLX_>)y$U3}-WkPXS1Dg zitkJDTWOSW(By8TVxfUg*I&=mu&GwZud1sPN4s|b^eJV&J%uuP_$_+N`o@W0rvO1i zXkA$;P_BK$+yJZE5L;LH_qoua`*-Q5pi5n1;K#0FCO{(Oa#Yu4C8v=FauUg4^#YE* zrCz18TAQBjcc0H`=q&F-t%>h)xt5$5`CmTUD!9m^)gyN6Pr4ag=UtfpvFf@;%fTI` zyv4qjvmr7$Hed|-2Um#wR~!0ux<3c8;-v!IpR{K%5Q;M(o09isw@m=K+%0%iK!>Nt zJNC7|M2%h&+=o9hZ-xrmhri?PjglYX4_3%7YwKuNH0TWUtlZcaakI@!pkzTj&?MX2 zRoQ-q_g858v5!}Bvr{5*OC*;^YXKg!z&7TjZ+Nj5_4i$v0>U~E^N}j~ijHcFy#{q()OKO}=w*~gmm;2jR;iA~-h_Nkkd_OitFggMdSWfziofd8G^pM{_9Od2rPqMsY!)1OP`KQf zV9T`ZX_?ly@5FxXZJ{^Z(h)79LNYY{?S&E-@A%sdk)t{^NW{f(%=%N?J;cue13vMx zq&dD0KV4>I??-FJQx524)VR2)8kh2`3@S%*jxN0uwLfW z6-~O8^Aisujer#g-%3d(<&53y)h)Ek$yt;(G}tF=Z63G&IOtHEDD5Y zdGU78QlHB;r;)YJ#6Bv;s~z1G@2B-Jaz4tGD!z8w4Ha6QKJfjWU<=xQ@bV{veI12L zkInc!zHfl`zmvCpTtIhIJ2*?|jvf5E5fwU94|erPp-e| zstik@Kjb0!d&=wl{UQxDFvu6u)<8|RJgO73v(Ggrh)-UE#V)Ln)9N=&-Mya(J1(V9X zZL7hN7az69SzNM`rE|@6d)>Y`+30!!GS| zmSo99zFL`kOW9(*fO!X&RX5%r)t@5B@8SJ#i@`s{lG=*Nx^vFS$KPez#(uboFRh%| zLD|V@a#>ZwJ1ivycES?*T2Of#(ORpCAy`8?a3#*@gy+S;>?+;{^mPAg@YUHgw1R2( zBlatbKba^GIkd{{^{&!TvwKq?W~T_kpKizXrnf-$fh$5kjd#rg-AlFZ1gX0@m8x{hmG6 zfdS2(<)52Fd(Aspb&-?2!JX_s5*>>>EKKGFJ2#l*fyXVz%&y*3Y^yY*{9v9f%2>o0 zBM)c1Wn|%i7f|-n5wvjlTz6n5UW#3+!`UtEXM9|nBK&O3&Y$==M@_z$TvRgl%|1G$ z^F`Tg*xdG~g`+d<5XtHq{nFk*A7%P#t>=wWXG5|Qarjq56uQJqk4`!3+HVx?|Kpx` zjMd{73?j2>8Y>4_s3#)-$^?~e2rw+ z9f}4y%VK0&2BXyp#%9Q0w}STO<7N8<<9C(@rPpH~$p^c!zwCNEp2CQv2S(f%1H0RI#4+LPB2SxQHiO4JF7;)2**?>6W;CEzVNJE` zh}Yk4jY)(Y#wls7h|_K$&j5R~NV+FErOU#l`GI_l33XC2kIn0{tiMe<<0qfuL19kI z*&hum5~&Zb^4ZJ$BFYm3+3tBc%*55mP|_jWE$Nhqtt}xiHk%-cSk`u?Hvk(3{=#z@z2 zIwl&_h3GG69b{yHSjn`q(&gkpcHSwmfOQY*%$^*1{CMhi@X0fT_dPc2_I6M=xZ)3F zkd&J>8Z%5U!#lh{@kpx}t?j&b5M)yK+^iMoYzkn*d5c!C&ee+LTEQ}^1&-FV{6tQ0 zfTp8%AH7iZAEn*)o|8Pp3@p!ph6X!~C1 zK;;3);NBGtR3!&(XlFQ$XSXV<&;#{3_`M>Aj0c$KO@V`w|9)UkjMx;4QmNt0@$%d{ z*>?&RPz^1gpB*%8LZm_}&{elgHPVTH8NcpQ?Y`u88Z@2V(9dx=g z`l`uhG9TQ87s$`*EHUZV-T-GE(KI!bvnap4Ss+tR0qo`7RKRBEuO=~?Kx4)fI`XbX z+i!KmO1$D;o5EB-Mu03^ppi+@xNeOtTVRt`IB+30&ONnXUut10I|kJ~z=qY_l7pC! zfCkKpe$`g~6<(P|<&wqKM>Fft!nb7_XD7ehBRu4w@;hAm4m5N=Ozjn#a)1_aNKcol z2pPY}agN8vOel2=-a=2ubcR6Ne|})??|4Fl5hIynCt@xgD%mCO@sqMLRZl)R$)eq3 zNB`}Sk}5M}N{=G2THq1z>|5nev=V7#j39JHmsIn(>*-G6#1Ea|H{q8ci7sn0s2_c9 zbC+E%J5EeS{2k=@b_^eG4RzXBa$kezIlDb_cAI@%fe9KFU$vC5_XxOJGsKKFvK zIM=l6N4dAFg>)f$nUBUQQ*bfnSGbGm3quwoX@811V|oF~CWps9{hX`ee@9R34hkMB zZ*;d#`A%MGiI9K{WrJP6SS>vrTeSxVnb1EhICY-fkGk=hc8S@i@EFo4PZ63b#FQ3% zlsl;o`>;;Se?W53C|Es7sB4OhDqEMp-!Cz24Zj2jHLR$5g>=9IG!VVtu_Fu#J zLY1}Q$*c6^t73=@&H#6Ozg^h+0TYAz@^Ewzg*9;Xa!>O)Y+<}!oVu>P2DOD%SN-pW z7Vw`V^VU3`JZV1D<9Bm}sV9YtuOqp~i*0g*D``-X3w-kr)5mDxE4$9=Bm8Hu$&R5m zI~BDTwKQ1HI5nMX{a?oe=KpnsIlA4t=OAg^TH?vkASe1}ogocisVnn#4-3kUq* zO%qYYWIm(vZ>BTR=d$>1xhtxdleu~X^AA~SdhNy#6Q>zjzY=PAyO3t`Mh|$y5SUvg z+fos5iow;|(Nf&03%RP)NeTMoZ76{{-%URY zwn3hBrfHL_dDv-@e??Ki3{v{#w30 z+Jl4Qv{bTOAcGM77}6p`ZlIK;3^x+Af+q0>+q}X(MGg5oR_$w*>iFZE941PI1y5Xu zG|zU7vczv&y%;db@A~N3vjzOh-t@M#`iOaGNh!q#@blt{$c>l58g z(jZ9_nkSV8g{U6Ce)s)6-{0@Lp1<~5>+Ew~uf6vFDd|s&MIZndYw)G8W?9yfrK;Qb=^uMjt(&<-U>2qk?@_NecgmJNrK!6~6zjBcw0% zpJ5@PKQEa3`T1B#3jAx&{=b$A&(tF!C87TtkmL*Z503KDoBdCzGJWNgFJvP0kN*cq z|9=Ag>;3`y*ZE&S|Azkn>HGXYpg;B>pg-1s0{sd61El{CkpBMy(*Far_;3`y z*ZE&S|AzknE&dOnKlUG>Kh}Q(&Hd9ue*%)c!M-v6;j{m{P?_%LyERaf-^o8RIy5{; z^RR%xbb+Pf+!p_H;Or9xw(pE0GScG2*sl=tKbEn!7#zW~pV#3Jt_%2hXd_Exy%e!p z7lElSUE$P%9prc1TWBA%U9Y$}5p^2IZCrEuBC&6P7yfOyx+T?5;)+i^#j)DYI??By**_cI>;Ph^B z_}mbKdgBPn=?6e-M=>;>(!#efiyi`S* z>k+~gaUJO0tIu%7ye0=Kk5j#$iBJ?ENNtw(0_R0J7|)Y{zAPc+{j36Wg!}1--~BA- zTQ;V3#^vZdkPbo@qN(*OJJfD@2K*0237@hFjPGm$DQ$xJKW~F=t~^M$jo{r!AE5n^ z1hp2S@T~JB#&tAe>CGs3(wPFI9t${B*AEhh?O;y9C2*CxM7q`HR~d3;<0NXH2(&=`&U7H z_cWLpDamfNZNV&Z6271A!mpw&xb8zYRzGUMch-_PWHdxft{4*2$^CF*>wQ#>6XATZ zt%2bnS&;iZ4Od^hPPYABO!_>M@#*L`2-fe0CtrU;U1UDmTMyAiO8d!|WyYYs$Q`%r zJc!mF)mUw71*XZ0P~Y*9wLv`>^QyWaH+eBJxTMIO`uvG8i!5R0#07(jP8Z!Ft3s1X zSEAayL3&oC2rnNv4nKW1q1MJ1SfbuRU-Wn3mE}utd1n9&w*G|992I<1%*!DuZtz$4 zT(-=$M%Wm80xoe4qSC!9_)10}=PoRRtjH|TH>6;9xC+$mW#Lz}5%}MY!F@j)Np=28 z!hawNa`t@#KCMJzG}#Y-N4w&^ctcDYJA~uk4};*LY-|kr23nozz&+83oWeBR?k z16jCsQ5t0F9wWBx2Vh3v6|>53*05So32Y^FpsU`E1`{hVxz0dm$~N>}=7YTtD7muC z4+FQ2o27RbQy2bnn6ryAJYVm_IA;O0sLEo=N)wR3*G5tg=y7^VuA}bxo5Zc-HOQX2 zk6&WTKsLq^m&o6T>sf@Fip7HFfoXpd!+&IC`^0Intc@TRAWR?4RKmN_i>6vwOY&OyOlj$a2;e7idca)YZ|V*KNqsISYWtMAC@Ze&}nsX==6INKF%+|=R4;^ z@ohnR^{&5Z!Qd+NtZ*f1lftmnA_1^*HWiE=1Y-)ikJy2;u$!v z=u4K-Ot{;&1d0wGBM}^VGFK*^mR)^iHX2^S`u3oZvQ<-IQ;G}D-j@fzR_q4@y{Bj} z8pIKEjlr<1E08&u1!6Cj!Ut0eP?V5B*Yb91B_Ik53hl^SR7HL+ari1%4F?GA(-Eu+Xi=7H5u%e%NJ~T>s!4rd5d_&FaTS-B}PVnGMp_UP6=$&89 zV63_pHihs)yU%{y)!c(Cn#`bk$tAi+nv$s01QxDzh8Jfpz?x~Im~b+N)=4Q~jkgWN zFU|&&zYieky^e*?M=-`a3CxDhk*cdjaB0d;dE^1JH+?0oM~tw6H}s`VdTlUpT^nZ98{V4Pd|E-S zx&*+_CC)50FMrVd#7!T?7ZuA{ zDRzfo!Bi#~^i)eRzhnn? z{+&;{{k!0%kOyY^xnbW!J52F)fvZ!0=*!L<;FM#I-1YJBJ&Y!VLE|Jk6Q~JGeW|#0;cBYEdy*s@6b7 z!g(x;F~OtnZktUDzeQI(Sq2HFVz4hP8YY{@iAUBr40akrgIfesTWp1|E`7j$b32s0 zS`0ave_^h`0Y*t63xq%Krb9~Sz%p(Y3QzR3rFl9K)7KYZU9|=4sH8M5MqBE*X(#M* ze@zRG^dRuW9&mhGNrwiGV#WytveO_2zP)Rp5d%t0`!)p{RGGxsLAD<#biCY7&06c=VC4gNu~G!~jAX(Dp9sC|?1?Rgyp-werPEh6 zBA3&0C{wsbXMQOMao1|1@9YV0V)jy>%#|?n-Z;Ka9;J6L^KqV~&jZ(vOdJ$8hb+TF zIDnz7yT667$)FZ`9~#m#zB24#nu_77I{f~6i3E3CqM8<8seg4U=Xa6ZN#0mzx_&}KB zKNoJ^b%%itDe_F$2h8lo&AyMmM4c}@5c5PIg9Fpy#z-|DzbFL9kLiNXQz^26Wkoa1 zmC)*b6}+9`$E~vSph^8WRhQ^Rr`{AY`YxNk%zDSvcdMehvpz>%T#LSUA0!tFStOc4 z{PEX3T+@DyZ2Z0hh^sDW-A%{X@7@rz)ePRA;N#4n!E@ownMTOG>WkAaj}pcE_Mp*I zP0RwmLzQAVX&Zipan)vM#4Ut}kJXYT+DhnE%gsLBvxL)l?>y`IQhs*WwGPtp{xxmt zJC2*bBtZ45^Du6GgbbUfK|}UVQu;2H%)j&*2d%nkPh~vkK-3sS^zFlXR<@ubs(Gn%9(IX9a}E!Uit8h~oJzA-BM(T(^E|wr zkpU+qQ*g;@afoy-fNe(>(MkWStdncI>Hf$2iSUnku=dtIA{2WF7Aj{_xBQE+zV`^e z4oe`cB@W=$$_=Blv|;_WamGE~3Uilsz?!WRxID`ef({Bp;ep>|#bFIdRZ655nF=st ziy?gSjWm-=;D`8ykBP&bgXr~a4`{u4ML++Dr{-@qW9sY=R95*2>B$d)=+ad3+$RU? z`GQel#%^X?KrxxKeLeOqSP!LY7pTXGHwho8C2hxdgX5SRdAZ{t3IFCu6#~{nTcjVH z>l@jX8UZZey>f!4gHly?&4?xTV75^{-5Q z9h?Ynv>xPMRv=4uoWhMpW#H9OPG&b((fv-vQ++W(z7{{E=JJUUy1EE?W=TPQl`CCas)|P*g`UQ;tI-M5rDGpm2mkN zKX5O9N=%ZjQ+XF-PRRyeTt3hUyoNhrp@%r^74*S(qo#EAuq?*9rXimw3$II`#(*F8 zIPiHUnCfqYsI~I2ooORQ?RS_{N2a4{5ySd+io*48ER60~$H5yCpj`c%L|(c|w~opH zTk#aFZ3F8$DwbNR+my0ZXYGmVM!e(~r||=jA+75i$mS zs|sQMD-jr|X`ljG--*=eO3F@pL~C4jvtsiP(s`{Qi)4b`?$VC~8?5%Zs8H@>{1jooY+@!3)<_TtTv`13vm3!l-zAC{b3y zwolhc<;SCF$#<8`m5zgqWg29YQ7&C)_!gRL{c+kX+Z zJ&eXUy99_Glp_u!8_C2g4YaLT$t)-`Mn;-2zFEfbUUoNiyDpFN!cO4RDox9?4M8o& z5Zi>s&}l<76HSy_3SGc#)61>E;L2s!t$8f_FYUaHFw`zSL#*z6D zUF|~^A2-9-3_t7&K8z9fe3)nJPY~V{d9WmOlH|O4$BfA;A^NM}!4(#`E!~kbqvaC` z4^E|W`BM0|?=En+>>#Z?byyK_k6te+rURcpk-ddsw5l?d5&v!gl@@=K7bJjo+x~AD5tHGYQ1qsp)ZTZ2#Hs@fkMae=Ke-0B6?tN4k~+3;d4iSwd&u9T`edM5 z9JhRw$0PIfz#9%QnmrqF{tPd0dh-}F%%Wh@-4}BEPqG|eo*;Z~Gr@IhHZ@V-4nv;t zXc(~)F1Xb(b5EaRseV-fyBK(l{-D=ES&p0Mpu@CjBz-goKWQ|OQC&+=>v0B&Bt0-1b%P_3>)`Lo zJeV}4)bM*N-TXZaGzIIJsDKhGmo~L_w~9j1swhl}ONATbqo};Fl1Y!7j?&*!;5m;i zdbuwnu`=gL`{YI9&@94fG1&}?SNB7|NDFi4*9F!NAwG0bC?+1y6Cn3z21a%Pa3CG* zgX7`I-Ay1kSBSGN`wjkB^^xrVaToP6R&gF|4us<6KJY-u0tZ4Hs7OHs9$eSO;yY4I zzOYxY7wFu>GKt-sRR{dgQS$?6-WsNAW1?)k@RR6VZOFc|!T@GCX2Z`F3hYUa0-p9V zqy?oK?8KLIIeJRdIc`@II2NUYxL87xJy^L5tF*)M(#Zt6AkCXPKTTuBzSLvOc>ZJ- z-3-A@b#2;ob3Mm5auKIv;x`?6?+gzUJ*jzKBCI@R3CH2SU^iX~ZV$~kcRp6b zH41oa{UIk$SWwgTc&Y2i# z{}TCvZ{ttNKHSqf8`epT(JKSO;CW4eQ^TADll3hqXWI_%qb|aP=LuZ?u^;_*2jh2} zt2lmTCK|sHf*}JFxaOh*(ZQ>5X3|YE`EdbQ-bkjsbN0|*)-$j;$pUomgu!j$3Gz&? zh3nE$_KnEF9S?nU`0hpPJGYRynjd7iA`3Q`wXy6*x*0*| z<18T|6@X71nj#tp)}7zl_?jB%z%@grtSg*eT%*u7IWQkQ7Yq}<0SR~%#RrSut6_lf zMItM592|6v;MGVbNP5NoIB5l053iWgi@np^?ns>a7yb3TThj-Y3?WaUq%2zHe5 zB|+ff0@!yt8LM+O@tpoRU3oPeA7yEy`-A0JTYH2GZ_T3l`#zEyJ3bnANs_!{iB09b zMDpEp59B#|5s^4?NI$F&3vOv4&m4OUvlfNS!YrWAyx`^So8+LmB8aSMfv{;g^h`<` z>y5@MQXeNV)%HX9%zz6l6JEj6zaLQ610FKy*TM3!QzmJAm!VZ*6czR;!?LNqsYtTM zbN4LChgN>d+meK}yenvNwl@r^u4L&oJHd_GcIrE}fSs!-Lt1}yLV>t4Y8(y5wL!d` zXvvxESXLhu+1!I4B>5=0^?=xJtp|;#`AqEs4le6f<*eSFgKH$u(k=22SZCkwAcOfv zG(hwlSe9O;hD#@L_ua>&=I&40aHNFp5fH*WVP6;?C769I8LZb4)Z`B0yox_Stn2hZ zJtGj}cJknZ?gZTFX#$O6i{VC&9E@5hp-tMVc^=N{c;?xH~A@l=?u(iDMt zmmZN-Pom&veF4>2nL)PB&n9Qxn`za`&A=1Y2=?Dav9VJV^yN;#e)VMhu`LSU_X@)m z)9Vbs+5ml*%@FVLeWbU=5Z68~LCcpLh@5HykteJ1HN?@9%{kz5_A>Q~GJ~T(Goe4x z3)Fn>khs;2%tK3n&5LGm!j8z%&s3Q#J)n&&?Y)o^DNc$$h``B1HDKWU6jfsOB43|M zn_u{Q>LVkI`@A%O1sjpCz78fP(y450G8z_sg6;Xwh)?}|+Ams%r;mET#pXnO)htC; zIWM7`#WnGA4u#SBIn(|!XB#)aI}`6z39v_=KHNT^y0le zFwQ4OFE;gJ;rdegQ!Eq08*h?GGaXER%){<6iAJ<4CQss;h)KjZ-1!%WwYMh*7KJpE z@5{5GCB>9Jk>5&vW}a@d?(ZTUV!JUTM-6u^KFfNm>JHJ78gQ-J0^58Fh&uC;K+JBa zKV(6A=j1`K@drk6p&+h3EzTA=GYJnBc4G6DbZlpu;m(m?5dQQaEaxv|1=InSU(5pb zjM)$p`vt7yrP*iGLg>?v74(pvB>R&342pVD}zXIGa;T`~|AvvBDTBH2Vm49v5j< z@EPFPDAR)e4iIcAM$Wo3W&@{f82ylVDs+k)LlWJftIZW{&Yh(Pmo?!1wbNkFqAxT` ze`VXE1;)6p<0xEH!h}z@a9UHHZTN#5xtjXTHVe8yXms)T-A8+BrZ#%?h9;#qPtPQ)p>If#jNn&sOK7&0=tI14UrUuWIMZl=OHrlN> zVUL9l;f>qJNan&V98b|$IJUxrZRw*;Gz;W8a$<&U4#WI3{BcxV6If)WWpXfh38|Wz3zsXZA?w;|V)#oEQZM+U{eyUHI%S6ahVry4 zXbl{=Vv0+*TqoRe&FEE^2eUd{A&C1VQ*`zjqfiio4qO^&*H`H|W)4NX-A!^qigKe%e>BohwKAY9n*x4z4R}(egyo@@L0<-C((7_>i5u)AHO|vn zT%FIzrM0dw+9XH1Zr-EmGl$7H!Diyq$-v+5!e|d)1!VD^g9goh{4(50ULU+cC90P} z{82V&b{0{y&JcKWgToZn8#6|Wxk>jyQ9S-2h8p#YbHo(-S%=D6=z=C$`k^2ds_SwH zw~{X`oE-%>>=u){&u@vdnu~%Lx}SZ!=7#>?6I1TnX{~+eEcuW|Gk&d zdU*`*?-7BmUBkp`H7{627~z165$^ibK`&Ta62C37WaOI;hR>HHwn0y!^xBd(!Gbc7 z{Mrs2TTwi#SVtWau8@MMdKYx}fPQ`N73H~7s+YfwjgQvv=~t zM9|5LF01#3h?nMgVtxpQSO37*H+F(m-8fUXZ#^}Z|BC)@lK9~KcGxX88^*u)pq8Q} ztVu0{%>Fg-?yM4y91|tFW5$rFnuw>T$i zcfJ;|TNavr?INygE12vaC6wFy7RPgEqDSma^8Ni|qI5=vqfsOY({789Ul%6GV=rEI z;Lu`b?!sEU;o zP1B)p@h-CH9v6B{q;Tf%499n}h%2Y^Re_&7t?Y=TZhL2dvr`aFzL7%n6cVXa&K;c7 zR7E61q;YF@3N?!kqxW1-(%Vjcpfj);e+6!XRV_PNj;b4|V~Ye6s4K{6tsG<|s@{^B z4VpN5bbg!f#q}UCb)l~jy$c)G#N(|cLF9DTY?8EMguc{h2A>6{kZ$I{{IvN9err=f z>t`soY`R26Z*GShA4^g1vNl}bdxJI%8kzOH5aXn9jS<^{bbLR-hF>NMcxO-$dVeXR zQ`S}DbS?!J&3sDt_6otQ?h5EXcZMYFE{B>8eRQPN3Am1w0uAEf9Eur5L+KJCy;~H0 z`PDGjxq`8D<0tFFrlE}2Es~X0MKbocn&}GEB3Fns{KevDExVqB*}>aT;>kwpdPf8s z{bi=k$MdjzHy;Um(nx}OlSwU8iS79*xJO+T6&;r_Nh7a`SBNIfc^Za&&aKS*SL?u4 zTLF*$l;;G7@^eI=?4*UEo*>Az9PPt5!l~kBa_hSyEM+X|&xw2@eJK#RqqsTt-g_>AH=j}C~uk~l)8Ta6IXQ-uzoSee`=5UXxjlCT<> zFJggacmsZ`$%XmeR#>{@8>(;LhpY3RV$y~*-1XoaJ<%ZrJM5Hc-&#Xx8XRMtt~)&? zI?;lbHKr)%oC@=7%E`0HJ^1x)2HB9W1s)IE+Bn`5lsm`<*=^kTH17-P5K)7fmO6BP zOEAR0yx-PoCkoP+KhkRlcGHYaQ+JQiV@#^6IzC*ohn2PB1zi-%hLPMuL`7YfLZ>X` z4SuDfSy8Zqqds-t8cwt31(1hzWpqRSF7)APqKj)8s!HWSU~b z@i}R{>;dl5&JaH;34edhCiyeAgK%IUxw1MQwCwdj=JtLN4mE>Q2{UNh=ACH8Nd_n1 zZ>%T>U1IJeh7sMfsg86Z$Ty|o4t0h$bGwk4Eh$8*pG9VsU&bH8-^k%NiNIUCjA$O< z{v!a$o1HMLJgfT$WEKEFLFab-EJ~C-5WgX6IntDeasoP zXUrH^87pd!H#3|k5A|7xnV+{ekb*aBpmk0zF+9-2>LrJneAY3Vqhp7z_0m}HkwdIx zO6kk1#b(Y~EhO<&7E^LE8{>G@VQ+UeS)#vrO0Y0ZKuKWQKZ1pSRb>AqSeSM~Js&(W zqfmUF6#IB_0F2zp!P8oYV5FoL9aLAbjgrf#eX=6QzR-@-YnDMr8hO}$BZu*U_YD#k zP{Mw7--(fbJCh@?_ZzlZ9mnxuZ|vOXil@4G*>U2VIL}As5?z_=n3e9smYc2%>?7^; z+)rMPySplU5Sz}H&!?znGoS6L@B_JC3$j&f3ZNv)7>Z&<*nJ*+9L;q+sQrMSU1$Ck zR)rmBH%j=i`R$e1TC!(wPK5ybvIm`-TpigvttfuyzliST`W&|#586cUxiHp>JZ%3J zI&9t&J6FK6o x^pB!ZQbuT|0Jo%skg%kng>U4>K-bN&{zB6Prf-<4@kd$r|En?0Vw$+X{{b52XpjH^ literal 0 HcmV?d00001 diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.mat b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.mat new file mode 100644 index 0000000000000000000000000000000000000000..281a9931cdbf19f7f091635676705c8992ebd1f4 GIT binary patch literal 11872 zcma)iX*3j$`@MY)2_bv7RLGXyBq0=0S+Wz#zHeh@vhOBYvnC0VA<1sYzGUBbGZ+j8 zgJBl)`+Q&g-~XR;o^zg8_uYN&J@?$_+OM8zKNeP!c_92;`<1lodrz19!Y@1>16_Um zz0`zX=vWvSKUBOgtmE(E80hj=*vDH<_|>~0;pdKF!ou>xau3wx9;(T!2+Kc^R}}vL z9E$%plm^e){<{_LQBZ^y1X?j#nk=lruieeOxv)DV6D{|tJzt!Tk^Pr#ri7@$ud*v; zaWU&(F-_uz*^{~Qv-zKf%&cx(dCN;IrF{OC+^8iqhLst^o)C+sG*LwX9cWam4Ttu1 zCOyW-?RyiocnhO-c*|N5obb@13QykLoA`#Gn>vE8!Elh(oF9;&tA16zzm2hZWi^B6 zGo|h`5Acuw^<t@bvJXbfx-iHim+A0`c_8NKUO>}M3t;$wIYPL1K`e5+6 zlusTGV%wg(>8U;ZyIM&VOejq6P zq@cf&Hn(^c#k9i^9>|X=ufcN#zR|7tf{f3qIs$hmygGWhn{TQBI}Haip}*^{>n!rc z63U`U-Cg|#aHTsBDH}W>U5|#Ho z+_yDx-){JFd%)=YX$+Xgnb!Yiy+k3krV$-#15~w+{fMqkG0H7&IH0%)SV)gPv+(#5 zQumU7^NR%P`?`%i)@&T-skQl)o0i+DLwHAd+<8i9><0?<(z4h(`BXMoB_W^@rb*dC zRV9O5j>fQkNDET-gN}>eKrvj2Ci%fv#*}@FOac~lUIz@A!hZ$4fYcWWD2 z^hpjLStCsv(=)&$U;;(-!jA9FXQ*|m^AZ+;Hnhc#8C~Vq zmj%vCE&ye=OC5LnnodjO0`AK`TKfw{o5550eC+~rJPQ<#pm z-QmjAgW2~XYy|#PNPn2uOlvM+lcx2C+j307tGR4T?zzS&Tcbizm~(M4HEI6sjnf(# zn@H0-McTt39?v47h-C3jk)Pwy=NSGEpv8riTG163+WkkqN%3n^{jQF-=N=3l4MFLh zsw)e8!6i@G!XP%z^L2Udy8O4=+5C*WmnGSW`R9|5;z88&(FlBAu(g-qyoCqASErtj zUiJM?WznK{fYowA!ds+OuDrYCrt`0@JDdLPoTZx_H=+Zo0iE7uHOIAlN*8hm;gjr( zZVvnhodh1@BgR4opt-WQ>4Pg#jlU6{9(@P*1R`Y@hsAabc3nR^K-;wOWGtPj!{HJ9 zgpLt%cj=)Pt$@8yuXa&=wWFj{dta@jBap<8KcF9YEw66%jBu)JGa0wv-}VqsvHJ3i zX3->z5%HNQ#&c|`sz!M-Hw$j$@=toM8^J9ZLd`0*@JHR(e%F7m@%`P+nk!Y7;1Z4F zJU0A!P&~;)=kSp|qRLP5_=?|pJyNjj0i?2NMCGhm^}=*57gXPUH)KEH-&>mz=IBBO z(A*8Op+#I|4McAW5H1#xQ`0a~SFI0?c3NLsSuERF#x!EOu{3CrEx$Do8=l$^A4fxAl+~E5)NXiq<0$J@5PE5WSC&M3mWdz#>oq=H=<| zgD8zy*6wxt@YB|rFOq)u5v6b2QZD34fN^;C-7a`fn@A_~gq!FI)5->?ubIKKC=he^ z7$rF?#B1!OkfgA3$(;PoOZ*kXahW!tuU#-rcYbY2iLta*8BzH_8b`GQS`)40oh3Pe#VKgqWmvEWyi_s))>9Q8PK`3PNB=SAaxPd~$#@F5xl@iZr)gZMe; zT#P4E8`mw(=)%fKk>Bw7NJmSPsz+LP@_sw=uPjmoi#7$G(1OPB9I{XeQ%py@L-~*b z+qgKYmzsPUvXw%g3XL|_l=oHN`MDAc4mqMC8uFizl*TbPn46Q5ijpf{BasL#XBM2cw3d7;ad+5 z*XH@de!qSBh$I_8ZTF77)kHpc;mZ`#oQ0(ahbUk=$+I(mhf;=A|) zKLRFz3X$vOEfY^BU%wbq!PbkMaW=By48s}`I}m9R$*!*C&`Ga5qo!geh?&;Xaj3s2 zRj^FlpVA0dBBh48Ke&my8D=8Zah^x5m1%CmQydZP$nEY&M>Jx(tD|*SMZc?Ph6Czo zznAwGzi`eeyWg7sL8Wp5b9*(=P{)Ry>T6_o3)X!6X5}1*#P9O())L6Uq$9#> zL}St7;jzVj)shmJ zX;XX~{NpvXU(MTaok}cPk9T|r zJmH^+_|)0BBM)s-z|mldH=83KE;4n{1hFG8T>Dshk62G@=Co)v(L%R59)y24h0-Ie zxY>NmHCBt_;Y`^k>?S=36U!VH{{=|cpD0jbr@-$<1Y>o)fAVUAmdhk(I=RvEz$gHt zK;Ks_Q|fFQCy5@bR0M9Oewnj!6HM`f- zB1tVNIK8w^DbvHG(6af5k1jMcF z_CjjGLuql~7{{MHIm-MF_LE;YHfuaVs*I=7z;2Dx^1^*}n|(@%Dg0@t>SYxra>nxf z_}lRuk58FV0@SIs-ZU4Ip>5Ml&h%51`WWITkM`55SW3qu81g?>? z8}oT%W?&y%Nr)Dr;A2)d@k;;`KIx7{Of6Wy+x*>&w*LuIL$fO* zGQq7fMBQP#7?qMyW^JKoztPE8|9##Yek#t?1eFFR5rAA1#j%c{Voo?=KG6?s>9O}5 zIHZ-)EI{}P{N%v4cxZT%e@qwFq1G82)`zr2L_U{Z&-4Gs68_3Vs3$B>g9|J+gKzn8 zrSy*j*Ap*ir}wQ^koDy43i(oe@0IEoAp#U_exqFQw<{?O$mFYCjE%Y+KW+X94) zHg!+FtDLVLBvr!ccg34RyySeJzF(m8vp?U!QHT9a^B-RWO5+!YoDS!z#PH9jRW~)= zyN8?f+p?ms65F07e~*33G#F;eY6jhr)v@e_?HPmc?{c=s1x}P z`qHTF;mvhyzd}TaF9z_57iYVg1W35YX5-$AKJMLvyYs29@C4`U%ui@q|2vt}Iw z)9FbjJcQWGBpCa?zEx9FSfqOt=DySB?P-z4CiPBr#{{mq{%>F`AfQLLg!~Ase6f;$ zmY&ZG&j2^Ff@oB)R0;5#9P?y9G5kk8D}xqyS1>B zK%$`a*&$yV|8~gV6E?R4GBX7QnS9?W%!VP1uXwqk<^`Go$%G!5NiKT^+Z@R*U5>l1 z`sUP8Ku+w_<5$+OwDfxGfh${IY?%fU%IPn{6!p{dv7M(x3E6c}zm^Xm|ewaFzBAFVyJc}Z$5*Sd z>3#%R=Z(y%WqPw9%C;3^zYwmoL z=5lS{7fB>6L-c5Dcw>??f> z$ZN4w5ikybDW6WLM`%W4n}ZQ}JBbCAu?^MFzcEfVF!wPMU$81;J7Vo`niEoKcU%?% z*nDbCH*djU7)k!tBYkVXxt5!>Idko5&b%$g_IJ=;*uI6mDvc`dr0zx6&TEZBY2rlN)MDoHg{>Q>tP^RiA}s3EK)Fp-Y&L{S<_EYPWniR80Lhc-BBRJ)&0O| zUEPlsO9-BtISKnNf&ldgzDlsvW<{6&Xm^d~(2&A^iKv4yYMGpTk-^{Vx1%tLVqZ^*e`LIZ~a?f5?ZABgmI-J&77yl0`_6mT&2T zxQ?vuE=B9`zjEZ=Kr4FEv>p8ijs{mYgsHL?nDOMtt&M`HDyicO-xq?1`5?;G*ZRsu z=&#O9o6vb*dO~sIzkaO#T;#no^Wh+keu*8Cc~&Yd7q6Q{Q4Pbt;Xiks*L9dr`&Bvh z0}z-$Y@tu(Ph*Q76F*H^;+h7H27p1Lf|x3EOfNy#ggpdtwd(f~TQ7@r+4|An^rLJ1 z<(<9E=j2baJ*mB$jZo|d^#c=T4Q>ggo_6`$Tus?{*86c_RQT<*o->KWCbA_9`90P` z+_5-vO2&aKi}gWv=ZAnlac%8PN~Vx3oH-oFj zo5vWsws&#nJuh`E@Xo_e`<(l<3iP4g$!B|mHYeS~x&xAXs_L77AT!ZEkF9sx&)upl z=j$e~MF`{mlbNSNeOyRTuj~FjOOsg8W{ky1RWVDa&yX>2PeHz7vc;SH;}=8QnzJb# z2qqm(`rV;5u3xtn)%3}3Ux)t=pR|;+gC=s<5p;S%`|*D@w(Yx15{{ z?6dnj$A)IxkK)fec`u*j4Yt)3r@9Kx{t+?$trQ*oMZffYXLG^%0n@5A#xS~Q3EL%l za_Ze#x2nk=oDqQ%j1tt<-u$Op6$v0&@r0pKN_%*-n@9;mO~XW)HRz@Kis^|EA4sXB=JQH$JONGnR*)L z8hE2Qs{V7l<_~18$s>ybYsfqcQN%`_xg*1~`Xg>8)NPZk;kC*p8pY=z6!hZZ{@10o zsFgAopoLEHh1t=EkHGZ@$Xa3u;^4ti3G_^_h-0;yT9&~g`HCK}RU}MqRAYlD(qq@T z!>%5zTf>N1{&5dQWbRUL2(?==&+1GZR#+;r(7BUs2;U8> z^CkxGml`iT2c$lA0jYRC*i*W+wkR+O$}%c}7)$IK*6C9oeU&()Tysyi{lo)EPLKo! z%rfyAc(b|H5quubf0Gm$>h5*gYB zyX{VXtqk15kMc?$ldeP6=R>xQPiF9n(<}Jz@f9A^TYWalcnRW9Iz5me{+-c%wB1o<_W3RXqOB*QLOG0~ZF1^l=vhZQ^l6!&XX1sAV=F6Bwxy5r3#&01aMS?j6U` z&jz6n#G2q|QMSF(ppxS76`rPvlfuv3e3oAh{|gkUWSN*(Yr#LlXjV=6$0}-Hl5{)k z+t#kBaGU3O_25WLUq?SC%|`c^*_8|k{TS9h%6Q8;7=Eu=j6ZmJG5hjMko565$)pcg zFY(*@2mPhvSm?Srydzsh;FzvyCcE0XP-Tx{?@>e3#hpV;!8{$1e=Yq(P#xBvM?b(* z1UC=vfvb5wKv({hsxVQ+RXg=n#nP_=>Ymum81mI?sm$I8wU|qJvYf>AJfaTlY$vwq zt@xf>Ce<_=!|@^Lk+x>EaYFD5_t6e*3^x*O6vtV$a7czyNrVu z#(6887qh9#o%RS5#}o`LMns>dH8p5>KD;wFc=dWPd)mEyg~DnDUWig{^wB;oX87g} zpJwn5u!p{=T0eqme61496y`Y1--juUT(>_+aw0fo z%nQcezX&_5=3@@-(mFX!-*?Msb+j)@XWo~7_Na@o|^xJ$3%YF>4@Q^Y!o*5kTEIB(ovi z5#oQ=jgv8YECLVaMNT2_?r|NXfkR8aX_q}}pNYBllo10aKTXRA2HC)-S&PP{w z*1cw4_0)U%(h_A@lVd^CcEtl^FIjeISlqh4i;vb;&~ImWp5qvPPx&6AR5z7+^NDBq z${WeatIu4y@fG)`tk#NT^=&KN9=aBb>QVJaIs1(MGtQ5)$n@y%bW1u`9>}5}SzuHb z1X8x2jbZ!*4_=6kN(BK}t~doyU%{DCOu`mPb*>RycC_L@6Cj30XzGjtN$2 znxfbwV-;wyzwX^Rt4*DvaQdJ$vln#giMwihDk3G4$JawMu+=c7qjIhJ8${vzKi{rx z@t!c?^uBlI1U_}@@R9yvXECQ=2R_;-(S+akH*(Xs<|rh$lyteGN=+(OyOJgxYH|#) z=|o#LN|ny9{Z{!!>u*0D4eCv+*7?Q*=_&LKrat?ksF;YYO#Uy4LneJ3+q$IAg;ULS zgBLrf&aJ_+j`X`gV3DXaJ*kTGjjJV$A zXsg(Kf@s5Mh!wmf7X1Tn+M*$7*zMECldkV0`iBZkyFT=g{eZFfU}#$GRm*!IegeWp ztZ58%7P4GQ#EvXv3`8p!Zw0Ki5A?g^Ztuy7rU%v6iJI-ZOhD>#teRW2!mna-*VQ&!2RdMR|gw3yUAd2tLlY2G-Ra`_EEJ^S$iAxGlDZ z&>q#~uDJ=`64KUuwmcE?4%w$ubTarUAhSy{p|Ox_M^X{SppjFa*0roteDF+*#XUaa zyCQ=wyylPlP;+*pI7vQSH0+C;+vu97g6f*5JU5E#zFpm6BI^h6@ z93>W2`WJcVEhl;{Qo5N5$)1>*a}vnC`_Wn7()VFh7QgJ$_5H5|ao17i;rox<5+IpT z0Iu#FzFJI+;WVFNX=y?~#5caf;NCqEfTay3B%vmm4H5Qe?Cc{zxaJmW&~iBRXyrpd z1$@+bS)53F^$~0p+45>ZHQ&#PYcygBtcGHm5b2CvKjO!kohy!%_rBaNaAp)K;2t9h zL+{BJY@;33| z2Cu%V%&mqqfxduGRT0lWE8aT4sbehym-=J9VX?4GMYia1DkO!U7*$UZv!kJ#fPgPh ze%s(={6j}Fz8gF$I=7esA4!uF>dleu1e;Dp-rFcuz3hJcw%y$839+r<89;V7F39ZL z5WYnvGT?6)mkR8Y`X|yJN^{-Ck4M1bAB4GNQLfL}j)$ zW3S8>fa|8f@mSC^QzhbU?~<(;NXf%!S?E2lRlaYtK|oa*M1ZN!{(HD=<3)eeg?oD+M>A$gThj^)O!byu{1Ru0=50ak_@4TY&CCVmpxG zI`&Gc(Q}MHRp;>YTum8gD+S%(WMhSTLQ+5Y9DtgY4?S)o+QXOgBarRa!pxg2X$umw zAbx4?a!abYAuNJ}N|{*s@<55)*2k)^M9u!E>P4Z788}kyB&tv597E!3VK(ma2Yj zlZEo^p!t8V3nW#va6MXlX_WMD4DJ$3;KR-x2Y)_?f)7$bGoK6!N`v+oNYj-ZDw60U zf#3{}yH^L~RqDAnn!wSJmx3bRGi=t8>ZBJY7xt=3G(_p=KnnGN$gm3am~^@kZj1I8 zu!M<+AFEVA8^p4bd#LV*n9o9x6sLl0D4pQ%-+cqckKy$LfRn$6of#2L0PWWvsk1Sbtaozbs*&HRzvWw@>ZthYPcZ;q;IX|}bE@;2nJX*Uf<+$- zK)-R@3=y$-3ks_QpjfTE|8p0tQX}Qx^Zo2V7k1MoEq0w31BR5adydK%LL#x`{@)A= z_=zr#h#&VS2A0<9vHB#T|AkA^*^DpDUvu`u5OldITTKt~@*&IG1HNIEkrgq`seC8n zd7RShIqXWH5051><2Lg&bUQVl*j!u>MbK3Ui^vG$JEv0~+#6g$5Nr$mSW#fy6&Xbw zYes2_#GE-CCGv~JWNVg9d+WmgRt0;MMMOBgD|}7;U2FlQ@P*72fdW?N54UExd!RE&Rnc>nPvGh29`T zpy{0EJj?39ujm4ym%coN+uZ!1&FSQx*ArZJ!lYFHbCeKIXEFosU16bxU2MUNf6hyfD;Spt)k5yF2?5h(bcEFFyy63OUA0mXn(r z#%6}sRg|^q>nMfN+W3?J{mnm!)JG5?E$M8lJ}m>6=Nh(-@d?ew;@*ry@V!g% z7nFfpL=lf8N`O= zXWQ|AuKG#8>=iZ(5*kd|W=PDJtxHb=8}JeE$Ts6@ac|S<6CT2_{J2$dZBp~MMqFFs z&-XIN=b_%(@!B${pH+72Xo=cBCB^d%drX&NfbSjO8`L z)e8%FCeGbXj_~_S+O%z8((`DaSM)FUkdJI!E8qn}{Y3`LPo$|j7}H0z|2g;Zo>(fr zI?tL4IKL;dFd`eIXUGzCZ zN%3|Nke4eJIU$K>N3ZmiHW@zM&!JrvD&{Rw(ahvXAy0I+n^cJxVF-rga{K9yk~X2dkb)GS z4u!i#58N84Z{g9qe4C_^3Yp9xQk-fj2$a*3*wff$fuaw9DO$^_>gQZ$l*?gNaYJgK z8adkZmA5ooIpWgveyMWVwy3=nYIwdOdxR^_r#!r5{{-(tGoc%BgF5`j>1x5dzBJ2` zKi`sj3iTkzS(5m>UabQmQla!9hiC9V>_w(I6BaRN*_gG|yC;9ljG)fyKHp^)Gc)!T zM5#0C1j1`;=IkWF?O@LvvoP9ADc$76;r*8qsEN4mZ8}4Rmm{WAvT@k$nztuYAzr1B zEIEO)w96C03RYk)b6%AYrcVBt{t|ro=c5`l?9SRur=3~-3vJLuz z(75@rGyZ6qmJm(V#`ExlQu{q|`Ti`);U=8Z`K^nQg=nK=$=)GM{Wqs`tCgS*boHb* zI#KdR8F3W-UcPZ=eQw&|87W_@@n-9ASU_VOMi2SXhn3jchh?oK|7WdUQ)`@-kg1oJ zwNL-ooz?hnLkp134h~HeJ)Vz7D0@<_UGGflaig0Wxt2I6el6nBAIeYRH}CIReH>w@ zI7u=KFx;(#iOI=QQ&==IwEhpnlInjLL1vJrFHL#cmlnT!8tCyvZb;)rYaPhC>4%?r zqqMKnMbUWV_C4xih`TQL_eFW86`y0%O+Bk-aMLs2Z94@N4YiU&qh))gYW8LPTjn38 zn4){MC79#Yur=H$4umQKDlmwAO1hq!^8Tb$m}my;`!Q4SxZ|I^>i|^y5(>M7$`ZG* z_X^uHFTRbrbEnGZxmrYAd%tt^t#~6<)Oi5&FVFei65uqlgmW)nZ`B3kpi!d2~zKu!VI^O=(X9p2lr-Lq`pciVC_kc566D zJ2i)X7uUzO(8Y7wu;;D31RWV;2dx+ko*x5%XFl-1nnIzYYp&-bzQ>Ib73^$yG?iFb7F>?_pEc_C40^>n_TIo^8W#4 Ch?9N* literal 0 HcmV?d00001 diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.onnx b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.onnx new file mode 100644 index 0000000000000000000000000000000000000000..7ca29df9db4d9f09aea5fea062103a227e436808 GIT binary patch literal 10601 zcmZ{qc~no|_x~$N8mL4mX`oOd&BNXMl_r%2N`|C?29iRh6cWuU$y|n%kkFun*FF1X zPKL}=MU*ijA(?-Dec$ij@ALhx_50(lyZ655uJu^=th@I)`#hxwC~@wSXShwa({cz2 zS*qn060|&WQDm6bjHsxH`BCv&_EC{5LYBvbEY}K+TCU~k;W1mwJt{aPLdz*?`I4X* zH7Vms6O1Pq>4+JNS#R@_v6Sh*C~|3RjEsEff`CZ@?m;o`u@M2Ylw|+IRr^mzN9w=F z$QaA~XIMt&?+cTIg9Gf8r2n-;aEf5U%)j0653&|mv6&|m96f&K>m0W$sv$oPK&8UF<``JX`l zx_^QGb^aI7zu~_?CjSBS*ZvFi*ZOauk$=C?-+)s8h@h1r%hmq-rXx8cC~~3F0FRKE zxTxie^>;{1OG?`+h}-?oiE~{mEir8+{0h9xYrUE+I{NiD4BfebUG==r5*kkk2l{TJ zjG3?DeZh68?%2#5+3REV)DfbJ!_7FQUX|8nxuDO{QJ5X)&Y|D{9a`4JrhIsZ3TJPD z;+hOnlshFH@Uj$zMxm&+E{}zK^%G?U{~}Gtmv}t6Z_M^odR09Kzx-Ii@?R9fpFl~L zajV@XC~ylDZ{*Bd}>^DaE@_#q17WQ1qEi z>3Wjf^DI-;b%@6&p@&)W-H&YMUL&}6M$n?f7AQRq> zq+_&2M@-VGV$lt%yE6dGdRN1a$y@p^KkmBQBx<*sK=|4NXB{!Zz3Y3qZ@nD*)@BEJ zZE~W~$MYamdOcKIRFhwjh0Xp)&*84<5ii%hgDI!AFb})Yv~s!+e!t9#N_W|?pDV@j z&zJQywAF_6MxTU776qKq^)-~(ag^@%76~p#WYEF7GPv^^@xtLkD)zLc+xin|-@{JU z6ZgZ=^S} zrfMasDEvqde&ykZiY++BazFEL%18Z^3Zf5r+v)HeErF?DJuCip=5&J0JNCiNke#}# zME1Lv(mo?CTrpxDQ@?nbmOM1V%J)4?t?E6K8KHzTYLQJ2+=P13RiLMO3ys1rGg%2{ROlnMUu}M(2FhWA246@TM#;{7J|zxL4UKv-^B1A8QFEM#J-%lf*}W6 zVX|I6oi&}0i>p)x*M|4t6spBfGv4ub9Rfk|SRrO@8&7lhH{#71JXXseMGZ#%ln1Duh|vlJ*~r(w{c5AbKgIn>`_D{U*S^-se5w@L)ea$Re?E5cON`)3&Yt@M#i zD$>G3Gi>qC^*GEbx{jvVpJ3Sc81z?j#QuU>cpo_S@=JADHYci+fxtEw> zq7I6_>tIr|JZ-$(!ZPz@F}x$3smI2Cu@|$NEzENfUhf z-5$5~w`0?Xox_!jN6_GN8tCA&o5pqk@q<4?RaPqIohpIwIU#J`WpP|NsT%iJdBNz# zh4|3*H!~Sig-MmEc)8;)|0d8MhsaN$=#RgJnxWgVVCfumI=`F!blU+pp9GNLkRncu zUc`L4QMjfu1alt>naPBkY*g@6Ji~V|1I1|cTi6SC61U<0pE;22ssk&M?laHCC?@6Y zN{hVr@N>SYp|P zTS$)>NGnw!2@Ia3c$dfe;8fWLr1Zp zc=)&wymF9^98#lc52lm*#2v6CESSy=zsB26&_{jySN!(1nYcS(Fr``%JU#lJeVn0< z?GLB2bvC-taeEbCp_PS8u4##UlXFpYrvO9mj;FlO-JJEVUKlW79j5Dd3rz#c< zv$}mdS-{>;Xs5V@c@}lBw6*DKTwm(#Nn$87SNML31M@sP4XgPW7~}ninR(yl z9jn_c^>2k^;fH3(@Cc^C)(dDru{umy^A7g7&7c8O&H;C7C|RiF!&7%`VB^-?&WN_`W6iImKELcw_>v6C5Zo)%m%kE zhTZj}&|_Z!;_g|jT5Ap~_*x8lBaXA0JN*O>Zwo2>_j~x&F&;k2RlpYKL=rQSL9Q6N z+rbjpnwdb;RvBY@ryn`ryvAMm^_q=%{+JUb`3i4Ls36nE8qjL9q&XuVqrfr~vx6&6 zpDwRQm(wXUbWJ9F8DNb+1eO$&-~?IWJ63)DTpS|cZ6s=D}vVXA;)FRLD3xCX{;hYA4WXL$QnK2)IZfCIB=?s3T z#!|MWEQnX0Wb@{Y<7MVsAsl+mrd^Q5mAdC?DVGX~kJV{)T@Y(Lxd0=o5tcZ1!^(kW zoT9D~&R8`Cd!+0sbGAHOS6Pq!oHsLd(Q?u7_d7A^!xT2RF%Xt$m9R@zN3m0E9M)`$ zMzh}}%~i!V2Uf{ znEh{M`hK~9Oq*1&X!<}H7p+9vmn2Z_t~I7v%_G$bJ8_Xr0vpg)$g18rkeJ3I-0P)G z#U8`K&nulhTRxE)Ze7HV>HGpqqhwrYKASSs8RzNEY@~h;18KQLoE!U+%{Je}nl22+ z9j9v94Rr@{kSSp|hK1n$+uO+K;aa}%xhLInFXH~dG_qV<2%4eo&?D;sZ_R?a$D4SN z5nN)n+Da_BGYO_f+~u(L@9*fnjDj!pxcH71JP`;?4EGoCWN zQ>pA;K_yg77>njwGND4($g2c}2~-VV2?n*wb%szZS!%;PZs zWqQMG4m4Q{bU5lPSDiZF=VAFJYf_mzhT7FOgSJK-T<-b~`p3?)F^bJ>#Dy}Nxju#_ z4ccJ6(V>w=`kGSl#uAWURLlh{U5BEBhLC6L!^zpDQ?uzIR&CrX^tYct+vpTcuDERd zCS(&^`$8H|>~~=UEp)K*<}w`LU5QEGhEu|PFRF803_+7VvaYrTf~%*llcPlf`Dm`B zq5^BGZvWGnn|JNU*uuL9oy2E^Zkj&pr%DfRcAUEX499+vjwG493e-v;HF%VfYnv zb>&gj%$mL=ycTMQ6|f&C3P7M{OcKwYG1X=3P9MAHi?3p2LCYf?TkGqX_=iB!XiKH) zSJ5OR+RcQ#5nA^X2Q!Uynt1*ZTiQLCGNxXJn06DCirv9&N@<3))5Ix!H^R{TSj^8m zgg2jkWLK7$(7h~YRI|McqkQ6UPu^{oXzj!6SY@DoNi}~h+Zr>+o)f;AQfCvX^Ih0K z+z!{2$oLvpEu=yl6kK;(~bAV?C@K^aHfroJ8KOdYIU84Lt_=;OC^Z zEc|Rap0|C>9Jk6rOMp6tw%mqnOBYn?y2ARuz6RBIMzRjkM(mnuhK@I0LD-u@K3y~# z;vSaK>99stD5FY$0_1UjXgd44?F7rPJi$51ThYjKwIr2U%p$9=Fq5V>?ww&JfB8=h zD^yY8vWg5*cYZY+u6Y=Lj4Xs-$4Z%Gq8rvMRVNMe95hsq!)N;?*{+L1%3L~tzQo;x zSqlLDdP6ACfP@9>S8+E_xS@4`8oqm?N2$|#xbgkOX>r0N4EGB|hX`-j)|rmi`XO78 zmXG6xxQ>uk14{d6_xtCdenubng&LsUp zpDs^44pSby1_SBI5Rr3`S>?%6VwwY1%V^P|mRd^q(hn8wtC)I(G=?tF#1s7(j1X(# z#zL%bDb0>&Rs}#ny+ySlpovhz|eR!R_8bhU{;6TK9 z%r>5k>zsD+uG41VLbJ^R2jwwdC{x2$Ji+4dbY6tTr9P{0Z%qB zzW-o_T{V)V^uQOR3lNx958vMMbVl1P(0-dsl3{NT|28W zI<}6T99)E^5%XDlnW=^2*B*ZMs*gC*!<#}U%TYwP0s1D%3GS9_(*}Ms99XiO1(pTj zOZIkwiTA~rbQC?f%lodfG z+jlZ^k5sgCPsg|2Hdys!D?9!<6Wc-}*~{Q=cxXNz8W&Ci*?0*&?xsfvy~7|=xr~1` z@)W2ZSdB6rXRVho9e(TU6cp)-;Z~R5ENZzPx<+RU7e9W<0=LP*;@`xF4X$MZ{Uf-x zE*caL+~;6g`E*6;K#Y0Xpue&Pfyk&lY^gGRD2*gueM>wT;8z6c3srDJBWPh zpE9lREyAfk?=sKOZM;`s-{DV_3;%eX46o3c%&S!7abqGI&;kni!_J4nv7{B6XUa2P zcD2A$Nsiy@nvG3wj^g>9F4(TJ6QN%-&73fd8<&|2IrC1@Z@El1d$c-68V|%8xrwyT z>jghx(C<13*g2Qh zsHDM++EmLa;$GKMmx1^DA;_5zH~IOFy|5ERa*o32P8SO_rMdaJ8m3Mz=T9T!SLcbL?|ClyRJOKj??K zy1J+sv;ys&@3HxPb^UkgW~g#rOt8&^56#x3MhPe0@%)v4!n7g>h%aSTWh4T|*16QTUvB^_sH7_ug~8=ND38R~U|7^cAe9 z%*OYnLh^SzjTU>>V{7tuW`10qdWWxu>y3JB2g-9Mx-rcEix=K~p<_KZbroLRc@};& z#|qcjG}8W+`)o8S-oO(a3;L;-+1BPpF9+R^;5IM)75=bv8i!{4S8u;xfDbUT%CwGqUR z-g%VW$=XE~ehqBi^fqc9>40Ni&Shdz`S|rBhr6p3$h7MN%X1nJ&+F@xCBpP)TX0aJ04-%k5GXAqa$kr>{VzaO_c%QCZ~$5cOvJ8X zHaI`j0nWbP08ZKdT!^F`_C9Ott3A)SJtKqB(BUUUF3pF>@dos*B!%r1W}?*>XMB9H zoz3ff151V`;mD{G+Nasf&(`Sz<*p6fg~6^6eW(|7t~=wPRbwbE(VKE{6_mG$V}-^( zGE%+D#!0t9D0{+QhiT*6TlToezzYi$2jiezPyWSYGfZFU&aOIchF7}kgV&br`Y}D5v@SYcf z2EN%?m!iyK3U!!l*F88p$A=uNH0i?4PPWivDa5QY#}7tcs1;d&^>3{(;bFSBl zBiz^5OhV#ZS(cX>taBh2{Hh(k71vM0)OIfbv5=oIo6W~^RG19p#O**!C9 zpwwP|DNM&=KPkG`s)BpVPVu%T>GxS z$j{GNp?)!IJ)MBZu2sV5%YLvm&=w4jB%}Imb>hDD^~Uu__VpQxx%g#M&^>1~b9LAN z55t^TazZ6|1rLU}SzUa5w}fcDZ7Ulv+>4gSW-{}J8Pq={4X*#tpg?yKtdp36lkDnY z&ld%L%aIgXYLmvkZ_`JKatGY_%AkUlk0(en`E;plsa=4U!PW{?)ntALXd)D$HS<{XD|FYU&*egq*J1G4STeHDaL-t z$9Tgh=vvuM;>us(+j^ie?nx|I%@`ZDbg|KW{dSX;ReXcgU^*INfuVj=Y4NN*F!jp{ zS}{cx=B?#v*Wz=mZR~Z3{543ZcvOi$WHAnt#I4Y0)>8Ln=k`a?QeL-M;u)Cyu)JSkR?G+EhC80nS+` zDcId#m#z;C#UFvA*_{_@C@pQkA5h(gZX>+WIch0RH|#nMhGOWxb{va;`v9}dAF;N&cr2ek zO!Rg<$C{@3Fy|Qo>_J@zHF&Aem4-uTo4bxJuH23ln>1+b6Ej>B8;JwGhCuG0xA3{; zA>0ew#YgTRNzRx~2NsHny6)|!FY?D&r=~2m)hN)u4{hf6ADe0_}t^LvXl ze(PG)8q{}S_(h67x29raimo6l`xoTe`;z_VBnntzf?2K~Y%Ux4u>0@(i?&A{K(%Ml zxN>3&-V4pb?$^ECZm%qO{Q3qps|>)}T@To>h1Kw+(}_y|*sxYEnNmu3V(~e1Dv2QW zbf6I_j=aXZ$Y){Am5of_@)MIUsDslAA$@yaef$l!Y~jBCFl5v~l#QK3!JVr>*2{$C zylXJG?>waK+yxky6p2f8hhwv401LjLOLxkPFzJnmwMNI|hpAg3iC>9U>RVvFgc8l@ zI}@ug8$u-(1llC?}0B1*HIp% z@ChfDkmp2kk)O*z^lmal#UnTR`XQCHEg%uZO+$i44ZsAl7)HYvQ`yy za=1MoUt=a6T(nC#ReHNnaHNcBTsw~s2572 zzgMvNewx@Y*Ol{@-Op;8hVbdxx1iah5+6PO%RzA8$X{j(89@yTE_TN-aD zTA*8q6}d^zr+f3x!QGu=`1#~``m}KhwPjrquH3ML6g0c}uRXG8CX)*f%S>=j#R~H8 zUno49-o%`rj-^0l2^yO`m!h>S@M^;>?7!QDhDdVU{uTGx`E(yL__c~G>R-d{wTV=I zFa_T=Ia|j^N`Ur^SXR)trg+&3G~~%qT3_P_4{lt9$h#U?Y*kK$WlET|GMm5T?nm(_ zD&c-(D(wG$o_#*~j3PFk0VmeLzgX#vPiq^vwnfsY@T-I@O6$yeR+Y+tW@#`w2*?$OkKrMwG|EPoef9%8= zHw7&DlOc9nFA){X-@tx52Ev|#73jHQA6p%zf~s!MU{&!KXf{$t&1pu=W^WtF+eYG_ zup*lWM;3wCOlBDUJo75^LxBWehvqM$fXA1j3)1cr3SLW}aO-I!Ic5~+;e z0V7WXUN4t~b(;*BNx^gI{A0!+>)W>_RLXFlAIjsSI61mt$#|c$`5>=U!nPlEp+jon zWEXj|JxlkPy|d=7`1U1!RVV=zd`g>*NT@J7cx<~1`c#R#64Bep#@%dVV?F) zPWkNt{$Zyw8V9<=n}#lKNMkuCoal^J&NY0NbO3n1E9N~9w!<=YTaLXR17$h8U|gVF zUnL!ngEL!U$Gn9|RvVzV?m4I}j0OLAeH28gidJsD3$LFlVraxKD4o@>Pp}{%ttBn- zk6__n71@6Y79<*GX$tbXxQ$CYkFdQbs%ZMcG*n$wMeP+HjNc43XGj{n0tEV zEZ%!;Opn*>LEZQaSYMZHF+XS>naW(osgI|Foa#I}^`IZv8jL5Ww`EuvK7z*P_>-r& zq^RO$GG|;PCJGimfnJ}+;LZH6P*LK-#zlR_SoiNRWOox(R}@l5wK%7*_V>H|*L?jW zsB@JrYZ=Xby4Az^YW<^VR8o-{DlM+0C?l&h&@L!u!9wpv2_Z5P(vtK0M*LOQ{r^Tt J*hwfz{~z@4C|3Xg literal 0 HcmV?d00001 diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m new file mode 100644 index 0000000000..f25709cd0f --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m @@ -0,0 +1,75 @@ +function t = reach_point() + + %% Reachability analysis of NAV Benchmark + + %% Load Components + + % Load the controller + net = importNetworkFromONNX('networks/nn-nav-point.onnx', "InputDataFormats", "BC"); + net = matlab2nnv(net); + % Load plant + reachStep = 0.002; + controlPeriod = 0.02; + plant = NonLinearODE(4, 2, @dynamics, reachStep, controlPeriod, eye(4)); + plant.set_tensorOrder(2); + + + %% Reachability analysis + + % Initial set + lb = [2.9; 2.9; 0; 0]; + ub = [3.1; 3.1; 0; 0]; + init_set = Star(lb,ub); + + % Store all reachable sets + reachAll = init_set; + + % Reachability options + num_steps = 30; + reachOptions.reachMethod = 'approx-star'; + + % Begin computation + t = tic; + for i=1:num_steps + disp(i); + + % Compute controller output set + input_set = net.reach(init_set,reachOptions); + + % Compute plant reachable set + init_set = plant.stepReachStar(init_set, input_set,'lin'); + reachAll = [reachAll init_set]; + toc(t); + + end + + t = toc(t); + + + %% Visualize results + plant.get_interval_sets; + + f2 = figure; + % rectangle('Position',[-1,-1,2,2],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1) + hold on; + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,1,2,'b'); + grid; + xlabel('x_1'); + ylabel('x_2'); + + f5 = figure; + % rectangle('Position',[-1,-1,2,2],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1) + hold on; + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,3,4,'b'); + grid; + xlabel('x_3'); + ylabel('x_4'); + + % Save figure + % if is_codeocean + % + % else + % + % end + + end \ No newline at end of file diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m new file mode 100644 index 0000000000..3b85b4601d --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m @@ -0,0 +1,75 @@ +function t = reach_set() + + %% Reachability analysis of NAV Benchmark + + %% Load Components + + % Load the controller + net = importNetworkFromONNX('networks/nn-nav-set.onnx', "InputDataFormats", "BC"); + net = matlab2nnv(net); + % Load plant + reachStep = 0.002; + controlPeriod = 0.02; + plant = NonLinearODE(4, 2, @dynamics, reachStep, controlPeriod, eye(4)); + plant.set_tensorOrder(2); + + + %% Reachability analysis + + % Initial set + lb = [2.9; 2.9; 0; 0]; + ub = [3.1; 3.1; 0; 0]; + init_set = Star(lb,ub); + + % Store all reachable sets + reachAll = init_set; + + % Reachability options + num_steps = 30; + reachOptions.reachMethod = 'approx-star'; + + % Begin computation + t = tic; + for i=1:num_steps + disp(i); + + % Compute controller output set + input_set = net.reach(init_set,reachOptions); + + % Compute plant reachable set + init_set = plant.stepReachStar(init_set, input_set,'lin'); + reachAll = [reachAll init_set]; + toc(t); + + end + + t = toc(t); + + + %% Visualize results + plant.get_interval_sets; + + f2 = figure; + % rectangle('Position',[-1,-1,2,2],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1) + hold on; + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,1,2,'b'); + grid; + xlabel('x_1'); + ylabel('x_2'); + + f5 = figure; + % rectangle('Position',[-1,-1,2,2],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1) + hold on; + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,3,4,'b'); + grid; + xlabel('x_3'); + ylabel('x_4'); + + % Save figure + % if is_codeocean + % + % else + % + % end + +end \ No newline at end of file