Airplane benchmark

verivital · Jun 18, 2020 · f7ba48d · f7ba48d
1 parent cf9342c
commit f7ba48d
Show file tree

Hide file tree

Showing 18 changed files with 577 additions and 0 deletions.
diff --git a/benchmarks/Airplane/controller_airplane.h5 b/benchmarks/Airplane/controller_airplane.h5
diff --git a/benchmarks/Airplane/controller_airplane.mat b/benchmarks/Airplane/controller_airplane.mat
diff --git a/benchmarks/Airplane/controller_airplane.nnet b/benchmarks/Airplane/controller_airplane.nnet
diff --git a/benchmarks/Airplane/controller_airplane.onnx b/benchmarks/Airplane/controller_airplane.onnx
diff --git a/benchmarks/Airplane/dynamics.m b/benchmarks/Airplane/dynamics.m
@@ -0,0 +1,79 @@
+function [dstates] = dynamics(t,states,actions)
+% Ex_airplane
+% constants as per the documentation Ix=Iy=Iz = 1; Ixz = 0; m = 1; g= 1;
+% description of the pararameters in these equations can be found here
+% https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf
+
+x = states(1);
+y = states(2);
+z = states(3);
+u = states(4);
+v = states(5);
+w = states(6);
+phi = states(7);
+theta = states(8);
+psi = states(9);
+r = states(10);
+p = states(11);
+q = states(12);
+
+Fx = actions(1);
+Fy = actions(2);
+Fz = actions(3);
+Mx = actions(4);
+My = actions(5);
+Mz = actions(6);
+
+T_psi = [cos(psi), -sin(psi), 0.;
+         sin(psi),  cos(psi), 0.;
+         0.,        0.,       1.];
+
+T_theta = [cos(theta), 0., sin(theta);
+           0.        , 1., 0.        ;
+          -sin(theta), 0., cos(theta)];
+
+T_phi = [1., 0.,        0.      ;
+         0., cos(phi), -sin(phi);
+         0., sin(phi),  cos(phi)];
+
+mat_1 = T_psi * T_theta * T_phi;
+
+mat_2 = [cos(theta), sin(theta) * sin(phi),  sin(theta) * cos(phi);
+         0.,         cos(theta) * cos(phi), -cos(theta) * sin(phi);
+         0.,         sin(phi),               cos(phi)];
+mat_2 = 1 / cos(theta) * mat_2;
+
+a1 = [u; v; w];
+a2 = mat_1 * a1;
+
+dx = a2(1);
+dy = a2(2);
+dz = a2(3);
+
+a3 = [p; q; r];
+a4 = mat_2 * a3;
+
+dphi = a4(1);
+dtheta = a4(2);
+dpsi = a4(3);
+
+du = -sin(theta)            + Fx - q * w + r * v;
+dv =  cos(theta) * sin(phi) + Fy - r * u + p * w;
+dw =  cos(theta) * cos(phi) + Fz - p * v + q * u;
+
+dp = Mx;
+dq = My;
+dr = Mz;
+
+dstates(1,1) = dx;
+dstates(2,1) = dy;
+dstates(3,1) = dz;
+dstates(4,1) = du;
+dstates(5,1) = dv;
+dstates(6,1) = dw;
+dstates(7,1) = dphi;
+dstates(8,1) = dtheta;
+dstates(9,1) = dpsi;
+dstates(10,1) = dp;
+dstates(11,1) = dq;
+dstates(12,1) = dr;
diff --git a/benchmarks/Airplane/specifications.txt b/benchmarks/Airplane/specifications.txt
@@ -0,0 +1,22 @@
+Initial states:
+
+x1 = 0
+x2 = 0
+x3 = 0
+x4 = 0
+x5 = 0
+x6 = 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]
+
+t = 20 seconds
+
+Property:
+
+x2 should be in [−0.5, 0.5] and x10,x11,x12 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
diff --git a/...hmarks/double_pendulum/Specifications.txt → ...hmarks/Double_pendulum/Specifications.txt b/...hmarks/double_pendulum/Specifications.txt → ...hmarks/Double_pendulum/Specifications.txt
diff --git a/benchmarks/Double_pendulum/Specifications.txt~ b/benchmarks/Double_pendulum/Specifications.txt~
@@ -0,0 +1,14 @@
+Initial states:
+
+x1 = [1.0, 1.3]
+x2 = [1.0, 1.3]
+x3 = [1.0, 1.3]
+x4 = [1.0, 1.3]
+
+t = 20 seconds
+
+Property:
+
+Each of the states should be in [−1.0, 1.7]
+
+Refer to this for more details: https://github.com/amaleki2/benchmark_closedloop_verification/blob/master/AINNC_benchmark.pdf
diff --git a/...controller_double_pendulum_less_robust.h5 → ...controller_double_pendulum_less_robust.h5 b/...controller_double_pendulum_less_robust.h5 → ...controller_double_pendulum_less_robust.h5
diff --git a/...ontroller_double_pendulum_less_robust.mat → ...ontroller_double_pendulum_less_robust.mat b/...ontroller_double_pendulum_less_robust.mat → ...ontroller_double_pendulum_less_robust.mat
diff --git a/...ntroller_double_pendulum_less_robust.nnet → ...ntroller_double_pendulum_less_robust.nnet b/...ntroller_double_pendulum_less_robust.nnet → ...ntroller_double_pendulum_less_robust.nnet
diff --git a/...ntroller_double_pendulum_less_robust.onnx → ...ntroller_double_pendulum_less_robust.onnx b/...ntroller_double_pendulum_less_robust.onnx → ...ntroller_double_pendulum_less_robust.onnx
diff --git a/...controller_double_pendulum_more_robust.h5 → ...controller_double_pendulum_more_robust.h5 b/...controller_double_pendulum_more_robust.h5 → ...controller_double_pendulum_more_robust.h5
diff --git a/...ontroller_double_pendulum_more_robust.mat → ...ontroller_double_pendulum_more_robust.mat b/...ontroller_double_pendulum_more_robust.mat → ...ontroller_double_pendulum_more_robust.mat
diff --git a/...ntroller_double_pendulum_more_robust.nnet → ...ntroller_double_pendulum_more_robust.nnet b/...ntroller_double_pendulum_more_robust.nnet → ...ntroller_double_pendulum_more_robust.nnet
diff --git a/...ntroller_double_pendulum_more_robust.onnx → ...ntroller_double_pendulum_more_robust.onnx b/...ntroller_double_pendulum_more_robust.onnx → ...ntroller_double_pendulum_more_robust.onnx
diff --git a/.../double_pendulum/double_pendulum_solver.m → .../Double_pendulum/double_pendulum_solver.m b/.../double_pendulum/double_pendulum_solver.m → .../Double_pendulum/double_pendulum_solver.m
diff --git a/benchmarks/double_pendulum/dynamics.m → benchmarks/Double_pendulum/dynamics.m b/benchmarks/double_pendulum/dynamics.m → benchmarks/Double_pendulum/dynamics.m