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/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