Get the linear_layer_width, negative_slope and bias flag.

generates a dataset using pybullet @param x_lo, x_up, bounding box on the initial states of the system @param dt float time s

Given the MIP is solved to optimality, get the indices of the active constraints. @param solution_number The index of the sub

Return ∂ẋ/∂x and ∂ẋ/∂ u

The control action should be u = K * (x - x*) + u*

Computes the next pose of the car after dt.

For state/control on the boundary of two modes, we regard that both modes are possible (because in numerical optimization we can't im

computes the reconstruction loss using either L2 loss or binary cross entropy @param x tensor label @param x_decoded

We replace the product between a binary variable α and a continuous variable x by a slack variable s, such that s = α * x. To impose this

computes the mean loss along a list of rollouts @param rollouts list of tensors, each one of them a rollout @param device whe

Solve the problem max_x V(x) − min_y V(y) s.t x∈∂ℬ, y∈∂ℬ where ℬ is the verified region (a box by default).

Compute the total kinematic + potential energy for a stance phase state.

We strengthen the big-M formulation of the leaky ReLU unit y = max(c*wᵀx+b, wᵀx+b), lo <= x <= up with the constraint y <= bc + b(1-c

Similar to train() function, but with given samples on initial_state and cost-to-go.

updates the parent of node[node_idx] to parent_idx.

To compute the maximal violation of the constraint that h(x) is negative in the unsafe region, or positive in the safe region, we

Compute the element-wise bounds on gᵢγᵢ return (gigammai_lower, gigammai_upper) gigammai_lower[i]/gigammai_upper[i] is the lo

@param model A ReLU network.

Helper class to train dynamics using lyapunov regularization @param train_dataloader torch Dataloader for training @param val

This function adds the constraint on zᵢ₊₁(j) = leaky_relu((Wᵢzᵢ+bᵢ)(j)) between zᵢ₊₁(j), zᵢ, and the (binary) slack variables.

Add the MIP constraints of the saturation block. Also output the bounds of u after the saturation.

Add a node with the path (x, u, dt) from this node to the parent.

The adversarial states generated from Gurobi often have clusters (some adversarial states are very close to each other). We select only one

This function is used in output_gradient_times_vector. It computes the lower/upper bounds of Wᵢ*z through optimization, where zᵢ is

Return the parameters (weights/bias etc) of the current model.

Compute the gradient ∂V/∂x. This function assumes x is a batch of state. When there are multiple possible subgradients, we ta

For an MILP, add the constraints such that we can compute V(x) = V_coeff * V_vars + V_constant Return: V_coeff, V_

Add the continuity constraint (8) in the documentation above cᵢᵀuᵢ,ⱼ+dᵢ = cⱼᵀuᵢ,ⱼ+dⱼ @param mode_i The mode i's index.

Overloads add_dynamics_mip_constraint in the FeedbackSystem class When propagating the bounds through LP, we form a big LP containing

This function is intended for internal usage only (but I expose it as a public function for unit test). Add sum_i ∂ReLU(x)/∂x

This function is intended for internal usage only (but I expose it as a public function for unit test). Add sum_i ∂ReLU(x)/∂x

This function is intended for internal usage only (but I expose it as a public function for unit test). Add sum_i ∂ReLU(x)/∂x

This function is intended for internal usage only (but I expose it as a public function for unit test). Adds ∑ᵢ ∑ⱼ sign(x(j)-

This function is intended for internal usage only (but I expose it as a public function for unit test). Adds ∑ᵢ ∑ⱼ sign(x(j)-

This function is intended for internal usage only (but I expose it as a public function for unit test). Adds ∑ᵢ sign(x(i)-x*(

Computes the gradient of the pre-touchdown state x_pre_td w.r.t the apex state (x position, height above ground at touchdown, and x

Compute the sum of these three losses 1. Loss of -h(x) on safe states. 2. Loss of h(x) on unsafe states. 3. Loss of -

@param eval_fun takes in the controller relu parameter and lyapunov relu parameter, returns a torch 0-dimensional tensor.

Compute the optimal objective as a function of MIQP data. If we fix the binary variable ζ, and take out the active linear con

Given x_lb <= x <= x_ub, compute the bounds on A * x + b by interval arithmetics (IA). Notice that this allows the computed bounds to be

After we have found the Lyapunov function satisfying the positivity and derivative conditions, i.e., V(x) > 0 and dV(x) < 0 for all

This is a utility function for output_constraint(). Given a network input x, this function computes the vector containing each ReLU u

First try to connect x_extend to each node in the neighbours, find the connection with the smallest cost-to-root from x_extend, add t

Compute max -h(x[n+1]) + h(x[n]) - ε*h(x[n]) as an MILP. The objective is −ϕ(x[n+1]) + (1−ε)ϕ(x[n]) + εϕ(x*) - εc

Take the sample state xⁱ, and compute the total loss on all these samples. Each state has a loss max(−hdot(xⁱ)−εh(xⁱ) + margin, 0).

Returns the gradient of the dynamics

Compute the dynamics gradient A = ∂f/∂x, B = ∂f/∂u

Compute the gradient A = ∂f/∂x, B = ∂f/∂u

The control law is u = -k*thetadot * (E - E_des)