Skip to content

Commit

Permalink
Merge branch 'master' of github.com:verivital/ARCH-COMP2020
Browse files Browse the repository at this point in the history
  • Loading branch information
ebotoeva committed Jul 3, 2020
2 parents 492fcdb + bbf5b4b commit 58ccf75
Show file tree
Hide file tree
Showing 11 changed files with 33 additions and 16 deletions.
2 changes: 2 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ ARCH Competition AINNCS 2020 -

- Unicycle (benchmark 10)

- Single Pendulum

- Double Pendulum

- Airplane
4 changes: 3 additions & 1 deletion benchmarks/ACC/Specifications.txt
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
Parameters:

a_lead = -2
t = 5 seconds
T_gap = 1.4
D_default = 10

Expand All @@ -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;
Expand Down
19 changes: 10 additions & 9 deletions benchmarks/Airplane/specifications.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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
Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf
3 changes: 2 additions & 1 deletion benchmarks/Benchmark10-Unicycle/Specifications.txt
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,12 @@ x3 = [2.1, 2.11]
x4 = [1.5, 1.51]

t = 10 seconds
control period = 0.2 s

Property:

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]
x4 = [-0.3, 0.3]
Binary file modified benchmarks/Benchmark10-Unicycle/controllerB.onnx
Binary file not shown.
Binary file modified benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat
Binary file not shown.
5 changes: 4 additions & 1 deletion benchmarks/Benchmark9-Tora/Specifications.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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]
The system, states 1 to 3, always stays within the box x ∈ [-1,1]


Binary file modified benchmarks/Benchmark9-Tora/controllerTora.onnx
Binary file not shown.
Binary file modified benchmarks/Benchmark9-Tora/controllerTora_nnv.mat
Binary file not shown.
14 changes: 10 additions & 4 deletions benchmarks/Double_Pendulum/Specifications.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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
Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf
2 changes: 2 additions & 0 deletions benchmarks/Double_Pendulum/dynamics.m
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@

th1 = x(1);
th2 = x(2);
u1 = x(3);
u2 = x(4);
T1 = T(1);
T2 = T(2);

Expand Down

0 comments on commit 58ccf75

Please sign in to comment.