Path_Following_unicycle.ipynb

{"cells":[{"cell_type":"markdown","metadata":{"id":"WBO8_ghrEFQ5"},"source":["# Learning Dynamics and Lyapunov function for Circle Path Following (Unicycle)"]},{"cell_type":"code","execution_count":null,"metadata":{"colab":{"base_uri":"https://localhost:8080/"},"executionInfo":{"elapsed":27852,"status":"ok","timestamp":1653519046186,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"-OnF__itEMS0","outputId":"696428e5-88a7-4c9f-b9e6-628a65581734"},"outputs":[],"source":["# To install dReal, if you use Google CoLab\n","# If not CoLab, command out\n","\n","import pkgutil\n","if not pkgutil.find_loader(\"dreal\"):\n","  !curl https://raw.githubusercontent.com/dreal/dreal4/master/setup/ubuntu/18.04/install.sh | bash\n","  !pip install dreal --upgrade"]},{"cell_type":"code","execution_count":null,"metadata":{"executionInfo":{"elapsed":3447,"status":"ok","timestamp":1653519049628,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"atGxNQ30EFQ-"},"outputs":[],"source":["# -*- coding: utf-8 -*-\n","from dreal import *\n","from Functions import *\n","import torch \n","import torch.nn.functional as F\n","import numpy as np\n","import timeit \n","import matplotlib.pyplot as plt\n","from tqdm import tqdm"]},{"cell_type":"code","execution_count":null,"metadata":{"executionInfo":{"elapsed":4,"status":"ok","timestamp":1653519049629,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"Z6d42dqWEFQ_"},"outputs":[],"source":["device = 'cuda' if torch.cuda.is_available() else 'cpu'"]},{"cell_type":"markdown","metadata":{"id":"-ABa4JuimH39"},"source":["## Actual dynamical system"]},{"cell_type":"code","execution_count":null,"metadata":{"executionInfo":{"elapsed":4,"status":"ok","timestamp":1653519049770,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"7a-XxCqy29Jk"},"outputs":[],"source":["def f_value(x,u):\n","    v = 1\n","    y = torch.zeros_like(x)\n","    y[:,0] = v*torch.sin(x[:,1])\n","    y[:,1] = u[:,0] - v*torch.cos(x[:,1])/(1-x[:,0])\n","    return y"]},{"cell_type":"markdown","metadata":{"id":"NQ0KBT6IEFRC"},"source":["## NN for the dynamics"]},{"cell_type":"code","execution_count":null,"metadata":{"executionInfo":{"elapsed":4,"status":"ok","timestamp":1653519049770,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"1X_2yo08EFRC"},"outputs":[],"source":["# NN for dynamics  1 hidden\n","\n","class fNet(torch.nn.Module):\n","    def __init__(self,n_input, n_hidden1,  n_output):\n","        super().__init__()\n","        torch.manual_seed(2)\n","        self.layer1 = torch.nn.Linear(n_input, n_hidden1)\n","        self.layer2 = torch.nn.Linear(n_hidden1,n_output)  \n","        self.to(device)  \n","\n","    def forward(self,x):\n","        sigmoid = torch.nn.Tanh()\n","        h_1 = sigmoid(self.layer1(x))\n","        out = self.layer2(h_1) \n","        return out"]},{"cell_type":"markdown","metadata":{"id":"TPdVl1pqEFRD"},"source":["## Learning the dynamics with NNs"]},{"cell_type":"code","execution_count":null,"metadata":{"executionInfo":{"elapsed":3,"status":"ok","timestamp":1653519049770,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"1qDlNfYz8dw-"},"outputs":[],"source":["with torch.no_grad():\n","    torch.cuda.empty_cache()"]},{"cell_type":"code","execution_count":null,"metadata":{"id":"9f3VTK43EFRD"},"outputs":[],"source":["# generate training dataset\n","N_f = 1801\n","xx = np.linspace(-0.9,0.9,N_f, dtype = float)\n","x_f = []\n","for i in range(0,N_f): \n","    for j in range(0,N_f):\n","        x_f.append([xx[j],xx[i]])\n","\n","x_f = torch.tensor(x_f)\n","x_f = x_f.float()\n","ut_bdd = 5.625  # bound for input\n","u_t = torch.Tensor(len(x_f), 1).uniform_(-ut_bdd, ut_bdd) \n","\n","# target\n","t_f = f_value(x_f,u_t)\n","\n","# input of FNN\n","x_train = torch.cat((x_f,u_t),1)"]},{"cell_type":"code","execution_count":null,"metadata":{"colab":{"base_uri":"https://localhost:8080/","height":311},"executionInfo":{"elapsed":149143,"status":"ok","timestamp":1652588621446,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"GLvIWIEOEFRE","outputId":"0c9cdef7-0a2a-40f6-ff1d-b5492e8a987d"},"outputs":[],"source":["# define parameters\n","max_iter = 1000\n","losses = []\n","# NN: 1 hidden layers with 200 neurons \n","fnet = fNet(n_input = 3, n_hidden1 = 200,  n_output = 2) \n","optimizer = torch.optim.Adam(fnet.parameters(), lr = 0.05)\n","\n","loss_func = torch.nn.MSELoss(reduction='sum')\n","\n","# # training\n","for epoch in tqdm(range(max_iter)):\n","    x_train = x_train.to(device)\n","    t_f = t_f.to(device)\n","    y_nn = fnet(x_train)\n","    loss = loss_func(y_nn,t_f)\n","    losses.append(loss.item())\n","    \n","    optimizer.zero_grad()\n","    loss.backward()\n","    optimizer.step()\n","    with torch.no_grad():\n","        torch.cuda.empty_cache()\n","\n","plt.plot(losses)"]},{"cell_type":"code","execution_count":null,"metadata":{"colab":{"base_uri":"https://localhost:8080/"},"executionInfo":{"elapsed":330,"status":"ok","timestamp":1653380190157,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"7-9AB0AgEFRE","outputId":"aa821244-8192-479a-8692-a961c2dc9a19"},"outputs":[],"source":["losses[-1]"]},{"cell_type":"code","execution_count":null,"metadata":{"colab":{"base_uri":"https://localhost:8080/","height":300},"executionInfo":{"elapsed":1485973,"status":"ok","timestamp":1653380153404,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"ZejzTU28EFRF","outputId":"ebdbd25b-ba26-4b72-d40a-d76fe3086681"},"outputs":[],"source":["# train more epoches\n","# fnet = fnet.to(device) switch between devices if needed\n","losses = []\n","optimizer = torch.optim.Adam(fnet.parameters(), lr = 0.001)\n","loss_func = torch.nn.MSELoss(reduction='sum')\n","\n","for epoch in tqdm(range(1000)):\n","    x_train = x_train.to(device)\n","    t_f = t_f.to(device)\n","    y_nn = fnet(x_train)\n","    loss = loss_func(y_nn,t_f)\n","    losses.append(loss.item())\n","    \n","    optimizer.zero_grad()\n","    loss.backward()\n","    optimizer.step()\n","\n","    with torch.no_grad():\n","        torch.cuda.empty_cache()\n","\n","plt.plot(losses)"]},{"cell_type":"code","execution_count":null,"metadata":{"colab":{"base_uri":"https://localhost:8080/","height":282},"executionInfo":{"elapsed":343,"status":"ok","timestamp":1653380184641,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"zEZ5v4Wh6lt-","outputId":"b246d969-bffd-4a75-ab4f-ef5ac7fa324d"},"outputs":[],"source":["plt.plot(losses[-500:-1])"]},{"cell_type":"markdown","metadata":{},"source":["### Generate testing dataset"]},{"cell_type":"code","execution_count":null,"metadata":{},"outputs":[],"source":["# parameters\n","r = 0.8 # region of interest\n","N_l = 1601 # change according to delta\n","xl = np.linspace(-r,r,N_l, dtype = float)\n","u_bdd = 5.  # bound for input"]},{"cell_type":"code","execution_count":null,"metadata":{},"outputs":[],"source":["# check the rough value of alpha\n","x_l = []\n","N_l = 1601 \n","for i in range(0,N_l): \n","    for j in range(0,N_l):\n","        x_l.append([xl[j],xl[i]])\n","\n","x_l = torch.tensor(x_l)\n","x_l = x_l.float()\n","\n","u_l = torch.Tensor(len(x_l), 1).uniform_(-u_bdd, u_bdd) \n","\n","# target\n","t_l = f_value(x_l,u_l)\n","x_bdd = torch.cat((x_l,u_l),1)\n","\n","# output of FNN\n","x_bdd = x_bdd.to(device)\n","t_l = t_l.to(device)\n","# fnet = fnet.to(device) # if need to switch device\n","y_l = fnet(x_bdd)\n","\n","# maximum of loss\n","loss_all = torch.norm(y_l-t_l, dim = 1)\n","alpha = torch.max(loss_all)\n","\n","# # infnity norm if needed\n","# dist = y_l-t_l\n","# loss_all = torch.linalg.norm(dist, float('inf'))\n","# torch.max(loss_all)"]},{"cell_type":"code","execution_count":null,"metadata":{"colab":{"base_uri":"https://localhost:8080/"},"executionInfo":{"elapsed":18665855,"status":"ok","timestamp":1653539068876,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"t2P6FCkW59GB","outputId":"b511660e-4647-47e8-fe4e-5081cd43f010"},"outputs":[],"source":["# check the actual value of alpha \n","# Remark (!): this box takes hours/days to run, please use the above line if you just need a rough value of alpha \n","\n","N_u = 50001  # 100001 corresponds to 1e-4\n","u_l = np.linspace(-u_bdd,u_bdd, N_u, dtype = float).reshape(N_u,1)\n","u_l = torch.tensor(u_l)\n","alpha = torch.zeros(N_l,N_l)\n","\n","for i in tqdm(range(0,N_l)): \n","    for j in range(0,N_l):\n","        x1 = xl[j]*torch.ones_like(u_l)\n","        x2 = xl[i]*torch.ones_like(u_l)\n","        x_l = torch.cat((x1,x2), dim = 1)\n","        t_l = f_value(x_l,u_l)\n","        X_l = torch.cat((x_l,u_l),1)\n","        X_l = X_l.float()\n","        X_l = X_l.to(device)\n","        t_l = t_l.to(device)\n","        with torch.no_grad():\n","            y_l = fnet(X_l)\n","\n","        torch.cuda.empty_cache()\n","        # target\n","        loss_all = torch.norm(y_l-t_l, dim = 1)\n","        del y_l\n","        max = torch.max(loss_all)\n","        alpha[i,j] = max\n","\n","alpha_max = torch.max(alpha)\n"]},{"cell_type":"code","execution_count":null,"metadata":{"colab":{"base_uri":"https://localhost:8080/","height":253},"executionInfo":{"elapsed":427,"status":"error","timestamp":1652681368565,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"apdf5UFPEFRF","outputId":"2de0d820-7a72-4013-cb15-c86b455ba224"},"outputs":[],"source":["# save the weights to calculate the Lipschitz constant with LipSDP\n","f_w1 = fnet.layer1.weight.data.cpu().numpy()\n","f_w2 = fnet.layer2.weight.data.cpu().numpy()\n","\n","np.savetxt(\"fw1.txt\", f_w1, fmt=\"%s\")\n","np.savetxt(\"fw2.txt\", f_w2, fmt=\"%s\")"]},{"cell_type":"code","execution_count":null,"metadata":{"executionInfo":{"elapsed":11022,"status":"ok","timestamp":1653519975652,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"AXBPyo9iEFRG"},"outputs":[],"source":["# save the fNN\n","# torch.save(fnet.cpu(), 'PF_fnet.pt')\n","\n","# load fNN from a file\n","# fnet = torch.load('PF_fnet.pt').to(device)"]},{"cell_type":"markdown","metadata":{"id":"cE9M7uUeEFRG"},"source":["## Plot the approximated results"]},{"cell_type":"code","execution_count":null,"metadata":{"id":"J8Wuhm0rEFRG"},"outputs":[],"source":["# dataset for plot\n","N_p = 300\n","xp = np.linspace(-0.8,0.8,N_p, dtype = float).reshape(N_p,1)\n","xp = np.concatenate((xp,xp), axis=1 ) \n","xp = torch.tensor(xp)\n","xp = xp.float()\n","u_0 = np.zeros(len(xp)).reshape(len(xp),1)\n","u_0 = torch.tensor(u_0)\n","\n","# target of plotting\n","tp = f_value(xp,u_0)\n","\n","# input of plotting\n","Xp_0 = torch.cat((xp,u_0), 1)    \n","Xp_0 = Xp_0.float()\n"]},{"cell_type":"code","execution_count":null,"metadata":{"colab":{"base_uri":"https://localhost:8080/","height":541},"executionInfo":{"elapsed":525,"status":"ok","timestamp":1652598187885,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"UOUDM486EFRG","outputId":"f2debd57-42f7-4ac0-a17c-bc2ccbd24634"},"outputs":[],"source":["# output of plotting\n","# fnet_1 = fnet.to('cpu') # to plot, command out this line\n","yp = fnet_1(Xp_0)\n","\n","with torch.no_grad():\n","    plt.figure(1)\n","    plt.plot(xp[:,0],yp[:,0],label='NN')\n","    plt.plot(xp[:,0],tp[:,0], label='y_actual')\n","    plt.legend(loc = 0)\n","    plt.xlabel('x1&x2 pair')\n","    plt.ylabel('f1')\n","\n","    plt.figure(2)\n","    plt.plot(xp[:,0],yp[:,1],label='NN')\n","    plt.plot(xp[:,0],tp[:,1],label='y_actual')\n","    plt.legend()\n","    plt.xlabel('x1&x2 pair')\n","    plt.ylabel('f2')"]},{"cell_type":"markdown","metadata":{"id":"Ll6LJcr-EFRH"},"source":["## Learned dynamics"]},{"cell_type":"code","execution_count":null,"metadata":{"id":"bJC54XLLEFRH"},"outputs":[],"source":["def f_learned(x,u):\n","    X = torch.cat((x,u),1)\n","    y = fnet(X)\n","    return y"]},{"cell_type":"markdown","metadata":{"id":"aoPCIEwoEFQ_"},"source":["## Neural network model\n","Building NN with random parameters for Lyapunov function and initializing parameters of NN controller to LQR solution\n","\n","LQR solution is obtained by minimizing the cost function J = ∫(xᵀQx + uᵀRu)dt, where Q is 2×2 identity matrix and R is 1×1 identity matrix"]},{"cell_type":"code","execution_count":null,"metadata":{"executionInfo":{"elapsed":143,"status":"ok","timestamp":1653519049769,"user":{"displayName":"Zhou Ruikun","userId":"16546965067278251021"},"user_tz":240},"id":"19ujoLFrEFRA"},"outputs":[],"source":["class Net(torch.nn.Module):\n","    \n","    def __init__(self,n_input,n_hidden,n_output,lqr,b):\n","        super(Net, self).__init__()\n","        torch.manual_seed(2)\n","        self.layer1 = torch.nn.Linear(n_input, n_hidden)\n","        self.layer2 = torch.nn.Linear(n_hidden,n_output)\n","        self.control = torch.nn.Linear(n_input,1)\n","        self.control.weight = torch.nn.Parameter(lqr)\n","        self.control.bias = torch.nn.Parameter(b)\n","        self.control.bias.requires_grad = False\n","        self.to(device)\n","        \n","    def forward(self,x):\n","        sigmoid = torch.nn.Tanh()\n","        h_1 = sigmoid(self.layer1(x))\n","        out = sigmoid(self.layer2(h_1))\n","        u = 5*sigmoid(self.control(x))\n","        return out,u"]},{"cell_type":"markdown","metadata":{"id":"6BkXJSg5EFRH"},"source":["## Parameters"]},{"cell_type":"code","execution_count":null,"metadata":{"id":"R_3Ujy7yEFRH"},"outputs":[],"source":["'''\n","For learning \n","'''\n","N = 500            # sample size\n","D_in = 2            # input dimension\n","H1 = 6              # hidden dimension\n","D_out = 1           # output dimension\n","torch.manual_seed(10)  \n","\n","r = 0.8\n","lqr = torch.tensor([[-2.4142, -2.4142]])  # lqr solution\n","b = torch.tensor([0.1974])\n","x = torch.Tensor(N, D_in).uniform_(-r, r)           \n","x_0 = torch.zeros([1, 2])\n","x_0 = x_0.to(device)\n","\n","'''\n","For verifying \n","'''\n","x1 = Variable(\"x1\")\n","x2 = Variable(\"x2\")\n","vars_ = [x1,x2]\n","v = 1\n","l = 1\n","config = Config()\n","config.use_polytope_in_forall = True\n","config.use_local_optimization = True\n","config.precision = 1e-2\n","beta = -0.1\n","# Checking candidate V within a ball around the origin (ball_lb ≤ sqrt(∑xᵢ²) ≤ ball_ub)\n","ball_lb = 0.1\n","ball_ub = r\n","\n","# parameters for beta\n","Kf = 45.\n","KF = 108.\n","d = 1e-4\n","loss = 0.007 # equals alpha above"]},{"cell_type":"markdown","metadata":{"id":"1XzUXGOvEFRI"},"source":["## Learning and Falsification"]},{"cell_type":"code","execution_count":null,"metadata":{"id":"wptWMdeVEFRI","outputId":"975ec332-bf43-4196-d87f-31eabb1f8460","scrolled":false},"outputs":[],"source":["out_iters = 0\n","valid = False\n","while out_iters < 2 and not valid: \n","    start = timeit.default_timer()\n","    lqr = torch.tensor([[-2.4142, -2.4142]])   # lqr solution\n","    b = torch.tensor([0.1974])\n","    model = Net(D_in,H1, D_out,lqr,b)\n","    L = []\n","    i = 0 \n","    t = 0\n","    max_iters = 3000 # increase number of epoches if cannot find a valid LF\n","    learning_rate = 0.01\n","    optimizer = torch.optim.Adam(model.parameters(), lr=learning_rate)\n","\n","    # learned dynamics\n","    f_w1 = fnet.layer1.weight.data.cpu().numpy()\n","    f_w2 = fnet.layer2.weight.data.cpu().numpy()\n","    f_b1 = fnet.layer1.bias.data.cpu().numpy()\n","    f_b2 = fnet.layer2.bias.data.cpu().numpy()\n","\n","    while i < max_iters and not valid: \n","        x = x.float()\n","        x = x.to(device)\n","        V_candidate, u = model(x)\n","        X0,u0 = model(x_0)\n","        f = f_learned(x,u)\n","        Circle_Tuning = Tune(x)\n","        Circle_Tuning = Circle_Tuning.to(device)\n","        # Compute lie derivative of V : L_V = ∑∂V/∂xᵢ*fᵢ\n","        L_V = torch.diagonal(torch.mm(torch.mm(torch.mm(dtanh(V_candidate),model.layer2.weight)\\\n","                            *dtanh(torch.tanh(torch.mm(x,model.layer1.weight.t())+model.layer1.bias)),model.layer1.weight),f.t()),0)\n","\n","        dVdx = torch.mm(torch.mm(dtanh(V_candidate),model.layer2.weight)\\\n","                            *dtanh(torch.tanh(torch.mm(x,model.layer1.weight.t())+model.layer1.bias)),model.layer1.weight)\n","\n","        # With tuning\n","\n","        Lyapunov_risk = (F.relu(-V_candidate)+ 1.2*F.relu(L_V+0.2)).mean()\\\n","                 +0.5*((Circle_Tuning-V_candidate).pow(2)).mean()+ 1.2*(X0).pow(2) + 0.0001*torch.norm(dVdx)\n","\n","\n","        print(i, \"Lyapunov Risk=\",Lyapunov_risk.item()) \n","        L.append(Lyapunov_risk.item())\n","        optimizer.zero_grad()\n","        Lyapunov_risk.backward()\n","        optimizer.step() \n","\n","        # neural Lyapunov function\n","        w1 = model.layer1.weight.data.cpu().numpy()\n","        w2 = model.layer2.weight.data.cpu().numpy()\n","        b1 = model.layer1.bias.data.cpu().numpy()\n","        b2 = model.layer2.bias.data.cpu().numpy()\n","        q = model.control.weight.data.cpu().numpy()\n","        b = model.control.bias.data.cpu().numpy()\n","\n","        # Falsification\n","        if i % 10 == 0:\n","            u_NN = 5*tanh(q.item(0)*x1 + q.item(1)*x2 + b)\n","            print(u_NN)\n","            vars_nn = [x1, x2, 5*tanh(q.item(0)*x1 + q.item(1)*x2 + b) ]\n","\n","            f_h1 = []\n","            \n","            f_z1 = np.dot(vars_nn,f_w1.T)+f_b1\n","            for n in range(len(f_z1)):\n","                f_h1.append(tanh(f_z1[n]))\n","\n","            f_learn = np.dot(f_h1,f_w2.T)+f_b2\n","\n","            # Candidate V\n","            z1 = np.dot(vars_,w1.T)+b1\n","\n","            a1 = []\n","            for j in range(0,len(z1)):\n","                a1.append(tanh(z1[j]))\n","            z2 = np.dot(a1,w2.T)+b2\n","            V_learn = tanh(z2.item(0))\n","\n","            print('===========Verifying==========')        \n","            start_ = timeit.default_timer() \n","            beta = np.maximum(beta, -0.1) # in case beta is too negative and cannot return any results\n","            result= CheckLyapunov(vars_, f_learn, V_learn, ball_lb, ball_ub, config, beta)\n","            stop_ = timeit.default_timer() \n","\n","            if (result): \n","                print(\"Not a Lyapunov function. Found counterexample: \")\n","                print(result)\n","                x = x.to('cpu')\n","                x = AddCounterexamples(x,result,10)\n","            else:  \n","                # calculate norm of dVdx with the SMT solver\n","                M = 0.5 # lower bound of M\n","                violation = CheckdVdx(vars_, V_learn, ball_ub, config, M) \n","                while violation:\n","                    violation = CheckdVdx(vars_, V_learn, ball_ub, config, M)\n","                    if not violation:\n","                        dvdx_bound = np.sqrt(M)\n","                        print(dvdx_bound, \"is the norm of dVdx\")\n","                    M += 0.01\n","                beta = -dvdx_bound*((Kf+KF)*d+loss) # update beta \n","                result_strict= CheckLyapunov(vars_, f_learn, V_learn, ball_lb, ball_ub, config, beta) # SMT solver\n","                if not result_strict:\n","                    valid = True\n","                    print(\"Satisfy conditions with beta = \", beta)\n","                    print(V_learn, \" is a Lyapunov function.\")\n","            t += (stop_ - start_)\n","            print('==============================') \n","        i += 1\n","\n","    stop = timeit.default_timer()\n","\n","    np.savetxt(\"pf_w1.txt\", model.layer1.weight.data.cpu(), fmt=\"%s\")\n","    np.savetxt(\"pf_w2.txt\", model.layer2.weight.data.cpu(), fmt=\"%s\")\n","    np.savetxt(\"pf_b1.txt\", model.layer1.bias.data.cpu(), fmt=\"%s\")\n","    np.savetxt(\"pf_b2.txt\", model.layer2.bias.data.cpu(), fmt=\"%s\")\n","    np.savetxt(\"pf_K.txt\", model.control.weight.data.cpu(), fmt=\"%s\")\n","\n","    print('\\n')\n","    print(\"Total time: \", stop - start)\n","    print(\"Verified time: \", t)\n","    \n","    out_iters+=1"]},{"cell_type":"markdown","metadata":{"id":"R48Y4MHLEFRJ"},"source":["### Checking result with a certain beta"]},{"cell_type":"code","execution_count":null,"metadata":{"id":"-HlQiJlUEFRJ","outputId":"ec497edf-3687-473d-eb47-ac6bc8563bda"},"outputs":[],"source":["beta = -0.1\n","start_ = timeit.default_timer() \n","result = CheckLyapunov(vars_, f_learn, V_learn, ball_lb, ball_ub, config, beta)\n","stop_ = timeit.default_timer() \n","\n","if (result): \n","    print(\"Not a Lyapunov function. Found counterexample: \")\n","    print(result)\n","else:  \n","    print(\"Satisfy conditions with beta = \",beta)\n","    print(V_learn, \" is a Lyapunov function.\")\n","t += (stop_ - start_)"]},{"cell_type":"markdown","metadata":{"id":"N7La9qY0EFRJ"},"source":["## Checking with beta = 0 for actual dynamics"]},{"cell_type":"code","execution_count":null,"metadata":{"id":"Z7v4iVINEFRJ","outputId":"33a916d6-3bd4-45c8-86c1-bb4bfc6bd1d1"},"outputs":[],"source":["beta = 0\n","f_u = [v*sin(x2),\n","     u_NN -v*(cos(x2)/(1-x1))]\n","start_ = timeit.default_timer() \n","result = CheckLyapunov(vars_, f_u, V_learn, ball_lb, ball_ub, config, beta)\n","stop_ = timeit.default_timer() \n","if (result): \n","    print(\"Not a Lyapunov function. Found counterexample: \")\n","    print(result)\n","else:  \n","    print(\"Satisfy conditions with beta = \",beta)\n","    print(V_learn, \" is a Lyapunov function for actual dynamics.\")\n","t += (stop_ - start_)\n"]},{"cell_type":"code","execution_count":null,"metadata":{"id":"USRli_vYEFRK"},"outputs":[],"source":[]}],"metadata":{"accelerator":"GPU","colab":{"collapsed_sections":[],"name":"Path_Following_unicycle_final.ipynb","provenance":[]},"kernelspec":{"display_name":"Python 3","language":"python","name":"python3"},"language_info":{"codemirror_mode":{"name":"ipython","version":3},"file_extension":".py","mimetype":"text/x-python","name":"python","nbconvert_exporter":"python","pygments_lexer":"ipython3","version":"3.8.12"}},"nbformat":4,"nbformat_minor":0}