From 5fac990c50f46c7cce2e4b108aeb924df641e009 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Fri, 19 Jun 2020 12:33:15 -0500 Subject: [PATCH 1/5] Update README.md --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 67c626e..a45aa8f 100644 --- a/README.md +++ b/README.md @@ -13,6 +13,8 @@ ARCH Competition AINNCS 2020 - - Unicycle (benchmark 10) +- Single Pendulum + - Double Pendulum - Airplane From f8d91e7009c7a4ee698747f6e88cd4d2987b16fe Mon Sep 17 00:00:00 2001 From: dieman95 Date: Fri, 19 Jun 2020 14:38:57 -0500 Subject: [PATCH 2/5] Update Sherlock benchmarks --- benchmarks/ACC/Specifications.txt | 4 +++- .../Benchmark10-Unicycle/Specifications.txt | 3 ++- .../Benchmark10-Unicycle/controllerB.onnx | Bin 14973 -> 15026 bytes .../Benchmark10-Unicycle/controllerB_nnv.mat | Bin 27244 -> 27236 bytes benchmarks/Benchmark9-Tora/Specifications.txt | 5 ++++- .../Benchmark9-Tora/controllerTora.onnx | Bin 84828 -> 84881 bytes .../Benchmark9-Tora/controllerTora_nnv.mat | Bin 154192 -> 154178 bytes 7 files changed, 9 insertions(+), 3 deletions(-) diff --git a/benchmarks/ACC/Specifications.txt b/benchmarks/ACC/Specifications.txt index 50bb15f..fcc4091 100644 --- a/benchmarks/ACC/Specifications.txt +++ b/benchmarks/ACC/Specifications.txt @@ -1,7 +1,6 @@ Parameters: a_lead = -2 -t = 5 seconds T_gap = 1.4 D_default = 10 @@ -13,6 +12,9 @@ x_ego = x(4) = [10, 11] v_ego = x(5) = [30, 30.2] γ_ego = x(6) = 0 +t = 5 seconds +control period = 0.1 s + Safety Property: x_lead - x_ego >= D_safe, where D_safe = D_default + T_gap * v_ego; diff --git a/benchmarks/Benchmark10-Unicycle/Specifications.txt b/benchmarks/Benchmark10-Unicycle/Specifications.txt index 4f7766a..e569119 100644 --- a/benchmarks/Benchmark10-Unicycle/Specifications.txt +++ b/benchmarks/Benchmark10-Unicycle/Specifications.txt @@ -6,6 +6,7 @@ x3 = [2.1, 2.11] x4 = [1.5, 1.51] t = 10 seconds +control period = 0.2 s Property: @@ -13,4 +14,4 @@ Prove that the system reaches the states: x1 = [-0.6, 0.6] x2 = [-0.2, 0.2] x3 = [-0.06, 0.06] -x4 = [-0.3, 0.3] \ No newline at end of file +x4 = [-0.3, 0.3] diff --git a/benchmarks/Benchmark10-Unicycle/controllerB.onnx b/benchmarks/Benchmark10-Unicycle/controllerB.onnx index 496f4bdb078877617b2c33f4a949032476faf976..c44f3b8caa49d46821c17f9df1cb6c8a6f26ddc7 100644 GIT binary patch delta 243 zcmexcvZ-`}FXR1ic)h*;|;lZ{R>iy5=%1k^Wu%-!%?|TLflBQQV7oE zX2$f%T8zBrMnVvCjHIBn5=#)!TrNAP`9?x~V0(<>-EtC3N>cNr!2HepO!L$w_R4cG zaeQIsVB}yFV01z_Wb+}-75oCS984&plglk@c{Gq5IQg%o9FH`zfQpq7y8;*3hRN|( FasXpcOkV&1 delta 225 zcmdl~`nP0)FXO6>evFJJGZ?wpic)h*;|;mEax(K$6N}=F;=_^HPC^_oaVaQkazA6b zstXrfTu1<>BHk@0v7{t5PYNos*@|hNy67%>4knH-%p8myi~@{KP-`}S&|JaKE5*Tt x5SqNgvX)a7X7^-6D>+UHI4|1DNL`5w!zLjAr3Ak4n`nma$*wT004XtK_dVF diff --git a/benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat b/benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat index f2602cebf5c15ba50295208245bf62990886e177..91174bfb297f1759b5f7861c65116ed0ccd5afd1 100644 GIT binary patch delta 103 zcmV-t0GR*m)B)tw0gyBpMsjH&N_B1^F*zVHF*-ChIx;yRGB7eQkx?U&Uh1`RFs;UlT%s>0C3O; JMzb$lJr5L3Bf0

g?G1H?r+shK%>rKt*u R3Pm7&0JI4RSFjl9`_uZxSDl%5@UrMv|36 z=1h)bDl#__f|z0=1*Mf(f`F!S*+ES=5#j^eViNC`lUP!cnkNP3H?LsczJi&tz(srw zGY2C_3J^02FghVzvR%i6aR#G+B)afLPex|O>3v>|ywmS_G0IHe4q~x*Ga9lhaDh#p JZs*M?2LLtnNH_oh delta 237 zcmbO@o%PN%)(O6h9UJ{-F`3O^(V6 zbOK3GI5YqN0C=3^V_;zL0Ae;E<^W S5R?J|0KIq$$hQMg0!<0&;3GZ& delta 126 zcmV-^0D=F)vnIyE>TGB7eQkx?U&U(V6 zbOK3GMnV7p0C=3^V_;wi0Ae;E<^W Date: Mon, 29 Jun 2020 12:23:39 -0500 Subject: [PATCH 3/5] fixed dynamics file --- benchmarks/Double_Pendulum/dynamics.m | 2 ++ 1 file changed, 2 insertions(+) diff --git a/benchmarks/Double_Pendulum/dynamics.m b/benchmarks/Double_Pendulum/dynamics.m index e73f643..0d953d5 100644 --- a/benchmarks/Double_Pendulum/dynamics.m +++ b/benchmarks/Double_Pendulum/dynamics.m @@ -10,6 +10,8 @@ th1 = x(1); th2 = x(2); +u1 = x(3); +u2 = x(4); T1 = T(1); T2 = T(2); From d95c84ce7e39e8aceb80e7e7aea351ccea5ab487 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Wed, 1 Jul 2020 10:56:10 -0500 Subject: [PATCH 4/5] Update specifications.txt --- benchmarks/Airplane/specifications.txt | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/benchmarks/Airplane/specifications.txt b/benchmarks/Airplane/specifications.txt index 7584a79..5aed4f6 100644 --- a/benchmarks/Airplane/specifications.txt +++ b/benchmarks/Airplane/specifications.txt @@ -3,20 +3,21 @@ Initial states: x1 = 0 x2 = 0 x3 = 0 -x4 = 0 -x5 = 0 -x6 = 0 +x4 = [0.0, 1.0] +x5 = [0.0, 1.0] +x6 = [0.0, 1.0] x7 = [0.0, 1.0] x8 = [0.0, 1.0] x9 = [0.0, 1.0] -x10 = [0.0, 1.0] -x11 = [0.0, 1.0] -x12 = [0.0, 1.0] +x10 = 0 +x11 = 0 +x12 = 0 -t = 20 seconds +t = 20 control steps = 2 seconds +control step = 0.1 Property: -x2 should be in [−0.5, 0.5] and x10,x11,x12 should be in [-1.0,1.0] +x2 should be in [−0.5, 0.5] and x7,x8,x9 should be in [-1.0,1.0] -Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf \ No newline at end of file +Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf From bbf5b4bdf7a5cc231959b6a73148e0e8c851c9b3 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Wed, 1 Jul 2020 11:03:07 -0500 Subject: [PATCH 5/5] Update Specifications.txt --- benchmarks/Double_Pendulum/Specifications.txt | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/benchmarks/Double_Pendulum/Specifications.txt b/benchmarks/Double_Pendulum/Specifications.txt index 15bfbea..30b7d58 100644 --- a/benchmarks/Double_Pendulum/Specifications.txt +++ b/benchmarks/Double_Pendulum/Specifications.txt @@ -5,10 +5,16 @@ x2 = [1.0, 1.3] x3 = [1.0, 1.3] x4 = [1.0, 1.3] -t = 20 seconds +t = 20 steps -Property: +1) controller double pendulum less robust: + - control step = 0.05 + - Property: + - Each of the states should be in [−1.0, 1.7] -Each of the states should be in [−1.0, 1.7] +2) controller double pendulum more robust + - control step = 0.02 + - Property: + - Each of the states should be in [-0.5, 1.5] -Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf \ No newline at end of file +Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf