At touch down, the post touchdown state is [l0;θ;-ẋsinθ+ẏcosθ;(-ẋcosθ-ẏsinθ)/l0;x+l0sinθ] @param pre_state The pre-touch

Compute -h(x[n+1]) + h(x[n]) - ε*h(x[n]) Note that we want this value to be <= 0

computes the dynamics loss in state space (this is just L2 on the predicted states)

Find the path between x1 and x2. We solve a nonlinear optimization problem. return the cost of the path.

Return the matrices Ain_r, Ain_zeta, rhs_in as torch tensors.

lqr control around the equilibrium (pi, 0). returns the controller gain K The control action should be u = K * (x - x_des)

Compute V̇(x) + εV(x) for a given x. Notice that V̇(x) can have multiple values for a given x, for two reasons: 1. Wh

This function only works when the gradient is unique.

resets the optimizers @param lyapunov_only boolean set to true to ONLY train the lyapunov. This is mostly useful for benchmar

@param symmetric_x If true, then we want the network satisfies network(x) = network(-x). This requires that bias=False, and the negative

In the stance phase, the state is [r,θ,ṙ,θ_dot,x_foot], where r is the leg length, and θ is the angle between the leg and the vertic

Given a point (linear_inputs, relu_activations), strengthen the big-M formulation by adding the constraints with the most violation e

For a flight state, computes the time to next touchdown on a given stepping stone. Returns None if the robot won't touch down on that

Transform the input to be A * x + b. Originally the constraints are Ain_input * x + Ain_slack * s + Ain_binary * binary <= rh

Compute the range of a linear layer output. We could solve an optimization problem (LP or MILP) to find (relaxed) bound of th

Add the dynamic constraints a mixed-integer linear constraints. Refer to relu_system.py for the common API. The constraints a

This function is intended for internal usage only (but I expose it as a public function for unit test). Add constraint lower

Add a new stepping stone to the terrain. @param left The left boundary of the stepping stone. @param right The right boundary

moves all the relevant parameters to device (e.g. 'cpu', 'cuda')

Returns true if the robot can touch down on a stepping stone with the given leg angle. False otherwise.

Similar to compute_output_gradient_times_vec_intermediate(), but the value of beta (the activation of the ReLU unit is given)

Compute the time derivative of the state.

In the flight phase, the state is [x;y;xdot;ydot], the dynamics is state_dot = [xdot;ydot;0;-g] @param state A lenght 4 numpy

generates a rollouts of the system using pybullet @return X_data, tensor [N+2,num_channels,width,height] @return x_data, tens

generate a single transition from state x0. A first image is taken at time t=0, then another one at t=.5*dt. These two images are the

compute the KL divergence from the samples produced @param z_mu tensor mean of the samples @param z_log_var tensor log of the

The lift off happens in the stance phase when the garud r - l0 crosses zero from below.

At lift off, the post lift-off state is [x_foot-l0*sinθ; l0*cosθ; -r*cosθ*θ_dot-ṙsinθ;-r*sinθ*θ_dot+ṙcosθ] @param pre_state

We assume that the Lyapunov function V(x) = ReLU(x) - ReLU(x*) + λ|x-x*|₁, where x* is the equilibrium state. Formula

Test the gradient of the MILP optimal cost w.r.t the ReLU network weights and bias. I can first compute the gradient through pytorch

Compute the cost as the summation of 1. hinge(-V(xⁱ) + ε₂ |xⁱ - x*|₁) for sampled state xⁱ. 2. hinge(dV(xⁱ) + ε V(xⁱ)) for sa

move all the parameters related to training the lyapunov to device @param device string for the device to move everything to

We want to compute the gradient of the network ∂ReLU(x)/∂x times a vector y: ∂ReLU(x)/∂x * y, and reformulate this product as

For a ReLU activation unit y = max(0, x), we can replace this function with mixed-integer linear constraint on x, y and β, where β is the bin

computes the reconstruction loss for a rollout @param rollout_expected tensor [N+1, x_dim] @return loss tensor of dim [N+1] o

Generate samples in a rotated box region R(θ) * (x* + box) where box is lower <= x <= upper

Strengthen the MILP for verifying Lyapunov derivative condition. The MILP from lyapunov_derivative_as_milp uses the big-M formulatio

We typically strengthen the big-M MIP formulation of the ReLU network with the following idea: 1. Relax the binary variables

full forward pass of the AE/VAE @param x tensor input @return x_decoded tensor, x encoded and then decoded @return x_

Visualize the depth measurement at the current time step and the next time step. Compare actual data with prediction. @param model_name:

Compute the element-wise bounds on Aᵢsᵢ Aᵢsᵢ = Aᵢx when the mode i is active. Otherwise Aᵢsᵢ= 0 return (Aisi_lower, Aisi_uppe

Args: mip_cnstr_return: Returned from mixed_integer_constraints() function. It encodes the constraint between x and x_next.

This function is used in output_gradient_times_vector. It computes the lower/upper bounds of Wᵢ*z through interval arithemetics (IA)ᵢ

The parameters to be trained.

Add the constraint (6) in the documentation above. s1 >= (cᵢᵀAᵢ+ε₂cᵢᵀ)vᵢʲ+cᵢᵀgᵢ+ε₂dᵢ @param mode_vertices mode_vertices[j] is

Add constraint (7) in the documentation above. s2 >= -(cᵢᵀ-ε₁*sign(v̅ᵢʲ-x*))v̅ᵢʲ - dᵢ - ε₁*sign(v̅ᵢʲ-x*)x* @param mode_index

Compute the next apex state, together with the gradient of the next apex state w.r.t the current apex state and the leg angle.

Given the active inequality constraints and the value for binary variables, compute the objective as a function of the MIP constraint