Compute u for a single state.

Given a point (xhat, beta_hat, y_hat), find the index set ℑ that best separates the point from the convex hull of integral solutions. Thi

We will generate a mesh of states within a range, and evaluate the cost-to-go for each of the sampled state. @param num_samples A length

@param TODO

@returns a Tensor between the initial state bounds of the training

Compute the gradient of the dynamics through autodiff.

Returns true if the polyhedron P*x<=q is bounded. Assuming that P*x<=q is non-empty, then P*x <= q being bounded is equivalent to 0 being

compute the output size of a list of layers, given an input image @param conv list of torch layers (like nn.Conv2d) @return t

Given the state right after lifting off the ground, compute the gradient of the next apex state w.r.t the post lo state. The apex

Compute the gradient of the lifoff transition function w.r.t the pre lo state. @param pre_lo_state The SLIP state just prior

Compute V̇(x) + εV(x) Due to the non-uniqueness of the gradient dV/dx, there might be multiple V̇(x) + εV(x). We return a lis

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

@return mixed-integer linear constraints MixedIntegerConstraintsReturn Ain_x, Ain_u, Ain_s, Ain_gamma, rhs_in,

Return the bounds on Aᵢx s.t Pᵢx ≤ qᵢ @param mode_index The mode index i @return (lower, upper) The lower and upper bounds on

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

Print the settings of this training device.

Loop through all the variables in self.zeta, if the variable is not registered as a binary variable in gurobi, then set its vtype to

gets a sample in latent space @param z_mu tensor mean of the samples @param z_log_var tensor log of the variance of the sampl

Set the objective. The objective is ∑ᵢ quad_variables[i][0]ᵀ * quad_coeffs[i] * quad_variables[i][1] + ∑ᵢ lin_coeffs[

This is the simple example from section 3 of Computation of piecewise quadratic Lyapunov functions for hybrid systems by M. Johansson and

In paper "Analysis of discrete-time piecewise affine and hybrid systems" by Giancarlo Ferrari-Trecate et.al. the authors define a piecewise a

Simulate the SLIP model from an intial state x0 in the flight phase. In the i'th flight phase, the leg angle theta is fixed to theta_

Compute the gradient of the stance dynamics function w.r.t the state. @param x The state in the stance phase. @return dxdot_d

Performs a single optimization step. Arguments: closure (callable, optional): A closure that reevaluates the model

Given the variables x_var, controller_slack, controller_binary (and the value of these variables stored inside x_var, controller_slac

Strengthen the MIP constraint on system dynamics. For ReLU network, we can strengthen its MIP constraint (derived from big-M

Given an MILP that verifies the Lyapunov derivative condition, we want to strengthen this MILP formulation, by putting constraints on

1. First formulate an LP relaxation of the MIP for the network. 2. Solve this LP relaxation. Make sure the solution is non-integral.

The touch down happens in the flight phase when the guard y - l0*cosθ crosses zero from above.

The math is explained in doc/linear_slip.tex Given a state right after touchdown, compute the gradient of the map from the po

Compute the gradient of the touchdown transition function w.r.t the pre touchdown state and the leg angle. @param pre_td_stat

For a given input x to a ReLU (including leaky ReLU) network, returns the activation pattern for this input. @param model_relu A ReLU net

The dynamics is ẋ=f(x)+G(x)u

Args: system: A continuous-time dynamical system. lyapunov_relu: The network ϕ(x) used in the Lyapunov function V(x).

Args: system: The dynamical system. barrier_relu: ϕ(x) in the class documentation.

@param system A AutonomousHybridLinearSystem or AutonomousReLUSystem instance. @param lyapunov_relu A ReLU network used to re

@param x_lo The lower bound of x[n] and x[n+1]. This is only used in forming the mixed-integer linear constraints. @param x_u

Give the samples, divide the samples to small batches, and run several epochs to reduce the loss on the sampled states.

Compute the range of beta_hat, such that max(c(w'*xhat+b), w'*xhat+b) <= min(x_coeffs*xhat + binary_coeffs*beta_hat+constants). A

Construct an MILP to solve the problem min V(x) s.t x in the boundary of the box.

For the region lo <= x <= up relu_input_lo <= w*x+b <= relu_input_up return all the vertices of the box lo <= x <= up if the vertex a

Return the mixed-integer constraints on a(x) and b(x).reshape((-1,)).

@params is returned from _get_current_training_params()

Add the dynamics constraints pos[n+1] = pos[n] + (pos_dot[n] + pos_dot[n+1]) / 2 * dt (rpy[n+1], pos_dot[n+1] - pos_dot[n], a

Test _add_constraint_to_program_by_layer with binary_var_type=BINARY