@return new_vars_list A list of new variables.

load from what was saved using the save method @param load_path string path to load dyn_learner from @param train_dataloader

Compute x[n+1] according to θ[n+1] = θ[n] + θ̇_dot[n]*dt when thetadot_as_input is true [pos_x[n+1], pos_y[n+1]] =

Set the linear objective. The objective is ∑ᵢ coeffs[i]ᵀ * variables[i] + constant @param coeffs A list of 1D pytorch tensors

Add linear constraints sum_i A[i] * x[i] <=, == or >= b @param A. A list of pytorch tensors. @param x A list of lists. x[i] i

Add linear constraint. @param coeffs A list of 1D pytorch tensors. coeffs[i] are the coefficients for variables[i] @p

Given a MixedIntegerConstraintsReturn @p mip_cnstr_return, add the mixed-integer linear constraints to the program. We assume

Compute the value of the Lyapunov function as V(x) = ReLU(x) - ReLU(x*) + λ|R*(x-x*)|₁ where |R*(x-x*)|₁ is the 1-norm of R*(

Add a new mode ẋ = Aᵢx+gᵢ if Pᵢx ≤ qᵢ @param Ai A x_dim * x_dim torch matrix. @param gi A x_dim torch array.

The output of (leaky) ReLU network is a piecewise linear function of the input. ReLU(x) = wₙᵀzₙ+bₙ s.t zᵢ₊₁ = max{0,

helper function to save relevant parameters @param save_path string for where to save (prefix)

Suppose the MIP is solved to optimality. We then retrieve the active constraints from the (suboptimal) solution, together with the bi

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

Set the Lyapunov function to be trained. We will train a ReLU network, such that the function V(x) = ReLU(x) - ReLU(x*) + λ|R

Returns the mode of x_start, u_start, namely self.P[mode] * (x_start, u_start) <= self.q[mode]. If x_start, u_start is on the

returns mean and log of variance in latent space as two tensors

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

Add a new mode x[n+1] = Aᵢ*x[n] + Bᵢ*u[n] + cᵢ if Pᵢ * [x[n]; u[n]] <= qᵢ @param Ai A x_dim * x_dim torch matrix.

Solve the optimization in the documentation above. If the optimal cost is 0, then we find a Lyapunov function. Otherwise we minimizes

This function is intended for internal usage only (but I expose it as a public function for unit test). we add the L1 loss |R

Compute the value of ϕ(x) - ϕ(x*) + c

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

Compute the index of α given an activation path (one and only one active ReLU unit on each layer). You could refer to output_gradient

Solve the MIP by constraining x[n] and u[n], the solution x[n+1] should match with calling step_forward(x[n], u[n]).

Compute xdot of the unicycle.

The controller is defined as u[n] = ϕᵤ(x[n]) - ϕᵤ(x*) + u*

For a ReLU network, in order to determine if the function V(x) = ReLU(x) - ReLU(x*) + λ * |R * (x - x*)|₁ where |R*(x - x*)|₁

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

Compute the input and output bounds of each ReLU neurons.

Compute the continuous-time dynamics

We will sample states xⁱ, i=1,...N, and we would like the Lyapunov function to decrease on these sampled states xⁱ. We denote l(x) as

computes lyapunov loss at the provided samples @param x_all tensor (num_samples, x/z dim) @param x_lo tensor upper bound outs

We will sample a state xⁱ, and we would like the Lyapunov function to be larger than 0 at xⁱ. Hence we define the loss as mea

Train a ReLU network on given state samples (not the adversarial states found by MIP). The loss function is the weighted sum of the l

Compute the Lyapunov derivative condition V(x[n+1]) - V(x[n]) + εV(x[n]) where the Lyapunov function is V(x) = ϕ(x) −

Compute the next state as pos[n+1] = pos[n] + (pos_dot[n] + pos_dot[n+1]) / 2 * dt (rpy[n+1], pos_dot[n+1]-pos_dot[n], angula

Parent class for encoders. Encoders should be child classes of this class and implement the forward method (which takes a tensor

TODO(hongkai.dai): I will deprecate this function soon. But for now I keep it for backward maintanence as other systems in relu_syste

We solve the MILP as verifier. If the MILP finds counter-examples, we add the counter-examples to the training set (with a maximal bu

This is the internal function to formulate an MILP for computing the region of attraction (ROA). Refer to compute_region_of_attractio

Take matrix R used in the 1-norm |R*(x-x*)|₁.

Compute the gradient ∂V/∂x. When the gradient is not unique, we return all the left and right gradient.

From a given node, try to forward simulate the states with many sampled control actions for time dt, and then return the state with t

Compute the total kinetic + potential energy for a flight phase state.

Pick out the active constraints on the continuous variables as A_act * r = b_act @param active_ineq_row_indices A set of indi

@param n Integer number of samples @return rand_data Tensor with random initial states @return rand_label Tensor with corresp

We will sample states xⁱ, i=1,...N, and we would like the Lyapunov function to decrease on these sampled states xⁱ. We denote l(x) as

compute the Lyapunov losses @param lyap_pos_threshold float the thresold used when computing an adversarial example for viola

generates a rollout with the learned dynamics for N step @param x_init tensor of dim x_dim @param N int number of steps to ta

The piecewise affine system is from "Analysis of discrete-time piecewise affine and hybrid systems" by Giancarlo Ferrari-Trecate et.al.