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 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/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 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 496f4bd..c44f3b8 100644 Binary files a/benchmarks/Benchmark10-Unicycle/controllerB.onnx and b/benchmarks/Benchmark10-Unicycle/controllerB.onnx differ diff --git a/benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat b/benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat index f2602ce..91174bf 100644 Binary files a/benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat and b/benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat differ diff --git a/benchmarks/Benchmark9-Tora/Specifications.txt b/benchmarks/Benchmark9-Tora/Specifications.txt index deac834..d862bc7 100644 --- a/benchmarks/Benchmark9-Tora/Specifications.txt +++ b/benchmarks/Benchmark9-Tora/Specifications.txt @@ -6,7 +6,10 @@ x3 = [-0.4, -0.3] x4 = [0.5, 0.6] t = 20 seconds +control period = 1s Property: -The system, states 1 to 3, always stays within the box x ∈ [-1,1] \ No newline at end of file +The system, states 1 to 3, always stays within the box x ∈ [-1,1] + + diff --git a/benchmarks/Benchmark9-Tora/controllerTora.onnx b/benchmarks/Benchmark9-Tora/controllerTora.onnx index 205ea50..f0fed8e 100644 Binary files a/benchmarks/Benchmark9-Tora/controllerTora.onnx and b/benchmarks/Benchmark9-Tora/controllerTora.onnx differ diff --git a/benchmarks/Benchmark9-Tora/controllerTora_nnv.mat b/benchmarks/Benchmark9-Tora/controllerTora_nnv.mat index 6422d51..7741afa 100644 Binary files a/benchmarks/Benchmark9-Tora/controllerTora_nnv.mat and b/benchmarks/Benchmark9-Tora/controllerTora_nnv.mat differ 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 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);