Inverted _Pendulum.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Learning Lyapunov function for Inverted Pendulum"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "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"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "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": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Net(torch.nn.Module):\n",
    "    \n",
    "    def __init__(self,n_input,n_hidden,n_output,lqr):\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,bias=False)\n",
    "        self.control.weight = torch.nn.Parameter(lqr)\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 = self.control(x)\n",
    "        return out,u"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Dynamical system"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "def f_value(x,u):\n",
    "    #Dynamics\n",
    "    y = []\n",
    "    G = 9.81  # gravity\n",
    "    L = 0.5   # length of the pole \n",
    "    m = 0.15  # ball mass\n",
    "    b = 0.1   # friction\n",
    "    \n",
    "    for r in range(0,len(x)): \n",
    "        f = [ x[r][1], \n",
    "              (m*G*L*np.sin(x[r][0])- b*x[r][1]) / (m*L**2)]\n",
    "        y.append(f) \n",
    "    y = torch.tensor(y)\n",
    "    y[:,1] = y[:,1] + (u[:,0]/(m*L**2))\n",
    "    return y"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Options"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "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",
    "x = torch.Tensor(N, D_in).uniform_(-6, 6)           \n",
    "x_0 = torch.zeros([1, 2])\n",
    "\n",
    "'''\n",
    "For verifying \n",
    "'''\n",
    "x1 = Variable(\"x1\")\n",
    "x2 = Variable(\"x2\")\n",
    "vars_ = [x1,x2]\n",
    "G = 9.81 \n",
    "l = 0.5  \n",
    "m = 0.15\n",
    "b = 0.1\n",
    "config = Config()\n",
    "config.use_polytope_in_forall = True\n",
    "config.use_local_optimization = True\n",
    "config.precision = 1e-2\n",
    "epsilon = 0\n",
    "# Checking candidate V within a ball around the origin (ball_lb ≤ sqrt(∑xᵢ²) ≤ ball_ub)\n",
    "ball_lb = 0.5\n",
    "ball_ub = 6"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Learning and Falsification"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(0, 'Lyapunov Risk=', 73.07650756835938)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-5.607981400644867165, -5.607370072610038392]\n",
      "x2 : [0.9742785792574937265, 0.974595727232512421]\n",
      "==============================\n",
      "(1, 'Lyapunov Risk=', 60.25868225097656)\n",
      "(2, 'Lyapunov Risk=', 53.768917083740234)\n",
      "(3, 'Lyapunov Risk=', 49.51911544799805)\n",
      "(4, 'Lyapunov Risk=', 45.072509765625)\n",
      "(5, 'Lyapunov Risk=', 40.94562911987305)\n",
      "(6, 'Lyapunov Risk=', 37.283748626708984)\n",
      "(7, 'Lyapunov Risk=', 34.052391052246094)\n",
      "(8, 'Lyapunov Risk=', 31.265596389770508)\n",
      "(9, 'Lyapunov Risk=', 28.827299118041992)\n",
      "(10, 'Lyapunov Risk=', 26.684879302978516)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.8167406192109095686, -0.8067406192109095597]\n",
      "x2 : [4.213750000000000995, 4.223750000000000782]\n",
      "==============================\n",
      "(11, 'Lyapunov Risk=', 24.627334594726562)\n",
      "(12, 'Lyapunov Risk=', 23.310089111328125)\n",
      "(13, 'Lyapunov Risk=', 22.142976760864258)\n",
      "(14, 'Lyapunov Risk=', 20.744461059570312)\n",
      "(15, 'Lyapunov Risk=', 19.24822425842285)\n",
      "(16, 'Lyapunov Risk=', 17.974822998046875)\n",
      "(17, 'Lyapunov Risk=', 17.215307235717773)\n",
      "(18, 'Lyapunov Risk=', 16.781858444213867)\n",
      "(19, 'Lyapunov Risk=', 15.697332382202148)\n",
      "(20, 'Lyapunov Risk=', 14.479691505432129)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-3.036726304977767299, -3.036327106010617616]\n",
      "x2 : [3.166088234611835972, 3.166405382586854778]\n",
      "==============================\n",
      "(21, 'Lyapunov Risk=', 13.542471885681152)\n",
      "(22, 'Lyapunov Risk=', 13.061758041381836)\n",
      "(23, 'Lyapunov Risk=', 12.441576957702637)\n",
      "(24, 'Lyapunov Risk=', 11.73182487487793)\n",
      "(25, 'Lyapunov Risk=', 11.130120277404785)\n",
      "(26, 'Lyapunov Risk=', 10.667765617370605)\n",
      "(27, 'Lyapunov Risk=', 10.418423652648926)\n",
      "(28, 'Lyapunov Risk=', 10.094032287597656)\n",
      "(29, 'Lyapunov Risk=', 9.645934104919434)\n",
      "(30, 'Lyapunov Risk=', 9.30141544342041)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-3.000762730418810698, -3.000000000000000444]\n",
      "x2 : [4.650657905674441928, 4.651292201624478651]\n",
      "==============================\n",
      "(31, 'Lyapunov Risk=', 9.007469177246094)\n",
      "(32, 'Lyapunov Risk=', 8.804839134216309)\n",
      "(33, 'Lyapunov Risk=', 8.625286102294922)\n",
      "(34, 'Lyapunov Risk=', 8.416444778442383)\n",
      "(35, 'Lyapunov Risk=', 8.200538635253906)\n",
      "(36, 'Lyapunov Risk=', 8.036065101623535)\n",
      "(37, 'Lyapunov Risk=', 7.908978462219238)\n",
      "(38, 'Lyapunov Risk=', 7.79890775680542)\n",
      "(39, 'Lyapunov Risk=', 7.686556339263916)\n",
      "(40, 'Lyapunov Risk=', 7.568135738372803)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.09148648242546728038, -0.0814864824254672715]\n",
      "x2 : [0.5226820961087009776, 0.5326820961087009865]\n",
      "==============================\n",
      "(41, 'Lyapunov Risk=', 7.931439399719238)\n",
      "(42, 'Lyapunov Risk=', 7.878018856048584)\n",
      "(43, 'Lyapunov Risk=', 7.796665191650391)\n",
      "(44, 'Lyapunov Risk=', 7.71148157119751)\n",
      "(45, 'Lyapunov Risk=', 7.6654815673828125)\n",
      "(46, 'Lyapunov Risk=', 7.613148212432861)\n",
      "(47, 'Lyapunov Risk=', 7.552687168121338)\n",
      "(48, 'Lyapunov Risk=', 7.494401931762695)\n",
      "(49, 'Lyapunov Risk=', 7.4583048820495605)\n",
      "(50, 'Lyapunov Risk=', 7.446130752563477)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-3.001525460837621395, -3.000000000000000444]\n",
      "x2 : [5.128917052002664789, 5.130185643902740011]\n",
      "==============================\n",
      "(51, 'Lyapunov Risk=', 7.386531829833984)\n",
      "(52, 'Lyapunov Risk=', 7.355416774749756)\n",
      "(53, 'Lyapunov Risk=', 7.333422660827637)\n",
      "(54, 'Lyapunov Risk=', 7.320272445678711)\n",
      "(55, 'Lyapunov Risk=', 7.296785354614258)\n",
      "(56, 'Lyapunov Risk=', 7.263550281524658)\n",
      "(57, 'Lyapunov Risk=', 7.240001201629639)\n",
      "(58, 'Lyapunov Risk=', 7.2231950759887695)\n",
      "(59, 'Lyapunov Risk=', 7.206154823303223)\n",
      "(60, 'Lyapunov Risk=', 7.186911106109619)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.008147664387664411631, 0]\n",
      "x2 : [0.4999336111575475305, 0.5064471316181660132]\n",
      "==============================\n",
      "(61, 'Lyapunov Risk=', 7.739080905914307)\n",
      "(62, 'Lyapunov Risk=', 7.727863311767578)\n",
      "(63, 'Lyapunov Risk=', 7.718023300170898)\n",
      "(64, 'Lyapunov Risk=', 7.7081756591796875)\n",
      "(65, 'Lyapunov Risk=', 7.697687149047852)\n",
      "(66, 'Lyapunov Risk=', 7.68766975402832)\n",
      "(67, 'Lyapunov Risk=', 7.677999973297119)\n",
      "(68, 'Lyapunov Risk=', 7.67039155960083)\n",
      "(69, 'Lyapunov Risk=', 7.665605068206787)\n",
      "(70, 'Lyapunov Risk=', 7.657990455627441)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-1.50914000225818179, -1.500000000000000222]\n",
      "x2 : [4.580816954259600671, 4.590816954259600458]\n",
      "==============================\n",
      "(71, 'Lyapunov Risk=', 7.520806789398193)\n",
      "(72, 'Lyapunov Risk=', 7.517190933227539)\n",
      "(73, 'Lyapunov Risk=', 7.512438774108887)\n",
      "(74, 'Lyapunov Risk=', 7.503897190093994)\n",
      "(75, 'Lyapunov Risk=', 7.4963884353637695)\n",
      "(76, 'Lyapunov Risk=', 7.492250442504883)\n",
      "(77, 'Lyapunov Risk=', 7.4855756759643555)\n",
      "(78, 'Lyapunov Risk=', 7.476679801940918)\n",
      "(79, 'Lyapunov Risk=', 7.470977306365967)\n",
      "(80, 'Lyapunov Risk=', 7.466259002685547)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-1.662043532690740122, -1.652043532690740335]\n",
      "x2 : [5.743258889954270252, 5.753258889954270039]\n",
      "==============================\n",
      "(81, 'Lyapunov Risk=', 7.446750640869141)\n",
      "(82, 'Lyapunov Risk=', 7.439898490905762)\n",
      "(83, 'Lyapunov Risk=', 7.434691429138184)\n",
      "(84, 'Lyapunov Risk=', 7.429951190948486)\n",
      "(85, 'Lyapunov Risk=', 7.424320220947266)\n",
      "(86, 'Lyapunov Risk=', 7.418050765991211)\n",
      "(87, 'Lyapunov Risk=', 7.4121198654174805)\n",
      "(88, 'Lyapunov Risk=', 7.407098770141602)\n",
      "(89, 'Lyapunov Risk=', 7.401872634887695)\n",
      "(90, 'Lyapunov Risk=', 7.395617961883545)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [0.1525748054893578398, 0.1625748054893578487]\n",
      "x2 : [-0.5261476940670223312, -0.5161476940670223224]\n",
      "==============================\n",
      "(91, 'Lyapunov Risk=', 7.905035972595215)\n",
      "(92, 'Lyapunov Risk=', 7.89856481552124)\n",
      "(93, 'Lyapunov Risk=', 7.8919172286987305)\n",
      "(94, 'Lyapunov Risk=', 7.8849358558654785)\n",
      "(95, 'Lyapunov Risk=', 7.877255439758301)\n",
      "(96, 'Lyapunov Risk=', 7.86959171295166)\n",
      "(97, 'Lyapunov Risk=', 7.862438201904297)\n",
      "(98, 'Lyapunov Risk=', 7.854935646057129)\n",
      "(99, 'Lyapunov Risk=', 7.846981048583984)\n",
      "(100, 'Lyapunov Risk=', 7.8391594886779785)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-5.948242885512812883, -5.946442184102795459]\n",
      "x2 : [0.1852144174109298103, 0.1877516012110795329]\n",
      "==============================\n",
      "(101, 'Lyapunov Risk=', 7.780818939208984)\n",
      "(102, 'Lyapunov Risk=', 7.759232521057129)\n",
      "(103, 'Lyapunov Risk=', 7.7544732093811035)\n",
      "(104, 'Lyapunov Risk=', 7.746870040893555)\n",
      "(105, 'Lyapunov Risk=', 7.736770153045654)\n",
      "(106, 'Lyapunov Risk=', 7.727166175842285)\n",
      "(107, 'Lyapunov Risk=', 7.718163967132568)\n",
      "(108, 'Lyapunov Risk=', 7.710120677947998)\n",
      "(109, 'Lyapunov Risk=', 7.701621055603027)\n",
      "(110, 'Lyapunov Risk=', 7.6948347091674805)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.7642169684594999346, -0.7542767678067869852]\n",
      "x2 : [3.000859375000000995, 3.010859375000000782]\n",
      "==============================\n",
      "(111, 'Lyapunov Risk=', 7.616725921630859)\n",
      "(112, 'Lyapunov Risk=', 7.608945846557617)\n",
      "(113, 'Lyapunov Risk=', 7.6005024909973145)\n",
      "(114, 'Lyapunov Risk=', 7.590701103210449)\n",
      "(115, 'Lyapunov Risk=', 7.58094596862793)\n",
      "(116, 'Lyapunov Risk=', 7.570881366729736)\n",
      "(117, 'Lyapunov Risk=', 7.5605058670043945)\n",
      "(118, 'Lyapunov Risk=', 7.553032875061035)\n",
      "(119, 'Lyapunov Risk=', 7.540709972381592)\n",
      "(120, 'Lyapunov Risk=', 7.531159400939941)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.7634029092622985901, -0.7534029092622985813]\n",
      "x2 : [3.000859375000000995, 3.010859375000000782]\n",
      "==============================\n",
      "(121, 'Lyapunov Risk=', 7.4513726234436035)\n",
      "(122, 'Lyapunov Risk=', 7.440633773803711)\n",
      "(123, 'Lyapunov Risk=', 7.4295477867126465)\n",
      "(124, 'Lyapunov Risk=', 7.418133735656738)\n",
      "(125, 'Lyapunov Risk=', 7.406391620635986)\n",
      "(126, 'Lyapunov Risk=', 7.394306659698486)\n",
      "(127, 'Lyapunov Risk=', 7.386124134063721)\n",
      "(128, 'Lyapunov Risk=', 7.370940685272217)\n",
      "(129, 'Lyapunov Risk=', 7.359564781188965)\n",
      "(130, 'Lyapunov Risk=', 7.347751617431641)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.7858355872212908766, -0.7758355872212908677]\n",
      "x2 : [3.000859375000000995, 3.010859375000000782]\n",
      "==============================\n",
      "(131, 'Lyapunov Risk=', 7.263988018035889)\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(132, 'Lyapunov Risk=', 7.250601291656494)\n",
      "(133, 'Lyapunov Risk=', 7.236979961395264)\n",
      "(134, 'Lyapunov Risk=', 7.223010540008545)\n",
      "(135, 'Lyapunov Risk=', 7.2086944580078125)\n",
      "(136, 'Lyapunov Risk=', 7.201108455657959)\n",
      "(137, 'Lyapunov Risk=', 7.1820502281188965)\n",
      "(138, 'Lyapunov Risk=', 7.169569492340088)\n",
      "(139, 'Lyapunov Risk=', 7.156250476837158)\n",
      "(140, 'Lyapunov Risk=', 7.142025947570801)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.1478872044539872865, -0.1378872044539872777]\n",
      "x2 : [0.4906053027858511828, 0.5006053027858511362]\n",
      "==============================\n",
      "(141, 'Lyapunov Risk=', 7.51865291595459)\n",
      "(142, 'Lyapunov Risk=', 7.506489276885986)\n",
      "(143, 'Lyapunov Risk=', 7.484013080596924)\n",
      "(144, 'Lyapunov Risk=', 7.466715335845947)\n",
      "(145, 'Lyapunov Risk=', 7.448116302490234)\n",
      "(146, 'Lyapunov Risk=', 7.429957866668701)\n",
      "(147, 'Lyapunov Risk=', 7.4117536544799805)\n",
      "(148, 'Lyapunov Risk=', 7.393825054168701)\n",
      "(149, 'Lyapunov Risk=', 7.374828815460205)\n",
      "(150, 'Lyapunov Risk=', 7.354898452758789)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.2026681702025549814, -0.1926681702025549725]\n",
      "x2 : [0.5115779157781130682, 0.521577915778113077]\n",
      "==============================\n",
      "(151, 'Lyapunov Risk=', 7.676586151123047)\n",
      "(152, 'Lyapunov Risk=', 7.652876853942871)\n",
      "(153, 'Lyapunov Risk=', 7.6282148361206055)\n",
      "(154, 'Lyapunov Risk=', 7.604683876037598)\n",
      "(155, 'Lyapunov Risk=', 7.57785701751709)\n",
      "(156, 'Lyapunov Risk=', 7.554262638092041)\n",
      "(157, 'Lyapunov Risk=', 7.5297136306762695)\n",
      "(158, 'Lyapunov Risk=', 7.503842353820801)\n",
      "(159, 'Lyapunov Risk=', 7.476127624511719)\n",
      "(160, 'Lyapunov Risk=', 7.447321891784668)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.2029357189846723308, -0.192935718984672322]\n",
      "x2 : [0.5115514807000420827, 0.5215514807000420916]\n",
      "==============================\n",
      "(161, 'Lyapunov Risk=', 7.718013763427734)\n",
      "(162, 'Lyapunov Risk=', 7.682585716247559)\n",
      "(163, 'Lyapunov Risk=', 7.651043891906738)\n",
      "(164, 'Lyapunov Risk=', 7.619380474090576)\n",
      "(165, 'Lyapunov Risk=', 7.586479663848877)\n",
      "(166, 'Lyapunov Risk=', 7.553680419921875)\n",
      "(167, 'Lyapunov Risk=', 7.523223400115967)\n",
      "(168, 'Lyapunov Risk=', 7.488954544067383)\n",
      "(169, 'Lyapunov Risk=', 7.459244728088379)\n",
      "(170, 'Lyapunov Risk=', 7.4271769523620605)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-1.007402139514671724, -1.003219481538011326]\n",
      "x2 : [3.940429687500000888, 3.943359375000000888]\n",
      "==============================\n",
      "(171, 'Lyapunov Risk=', 7.285134315490723)\n",
      "(172, 'Lyapunov Risk=', 7.252197265625)\n",
      "(173, 'Lyapunov Risk=', 7.234084129333496)\n",
      "(174, 'Lyapunov Risk=', 7.189773082733154)\n",
      "(175, 'Lyapunov Risk=', 7.160049915313721)\n",
      "(176, 'Lyapunov Risk=', 7.131477355957031)\n",
      "(177, 'Lyapunov Risk=', 7.100903511047363)\n",
      "(178, 'Lyapunov Risk=', 7.068724155426025)\n",
      "(179, 'Lyapunov Risk=', 7.036521911621094)\n",
      "(180, 'Lyapunov Risk=', 7.01576042175293)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-1.074777755609998442, -1.066472630430395974]\n",
      "x2 : [3.973515625000000995, 3.983515625000000782]\n",
      "==============================\n",
      "(181, 'Lyapunov Risk=', 6.886301040649414)\n",
      "(182, 'Lyapunov Risk=', 6.858092784881592)\n",
      "(183, 'Lyapunov Risk=', 6.829318523406982)\n",
      "(184, 'Lyapunov Risk=', 6.799976825714111)\n",
      "(185, 'Lyapunov Risk=', 6.7697672843933105)\n",
      "(186, 'Lyapunov Risk=', 6.7389607429504395)\n",
      "(187, 'Lyapunov Risk=', 6.707645893096924)\n",
      "(188, 'Lyapunov Risk=', 6.683724880218506)\n",
      "(189, 'Lyapunov Risk=', 6.647182464599609)\n",
      "(190, 'Lyapunov Risk=', 6.617501258850098)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.2066932182253851391, -0.1966932182253851302]\n",
      "x2 : [0.5112039339275974426, 0.5212039339275974514]\n",
      "==============================\n",
      "(191, 'Lyapunov Risk=', 6.757404327392578)\n",
      "(192, 'Lyapunov Risk=', 6.724518775939941)\n",
      "(193, 'Lyapunov Risk=', 6.690707206726074)\n",
      "(194, 'Lyapunov Risk=', 6.656280517578125)\n",
      "(195, 'Lyapunov Risk=', 6.621293067932129)\n",
      "(196, 'Lyapunov Risk=', 6.592226982116699)\n",
      "(197, 'Lyapunov Risk=', 6.5529608726501465)\n",
      "(198, 'Lyapunov Risk=', 6.520031452178955)\n",
      "(199, 'Lyapunov Risk=', 6.48593282699585)\n",
      "(200, 'Lyapunov Risk=', 6.450390338897705)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.208504925845939354, -0.1985049258459393451]\n",
      "x2 : [0.5110359584392712984, 0.5210359584392713073]\n",
      "==============================\n",
      "(201, 'Lyapunov Risk=', 6.556550025939941)\n",
      "(202, 'Lyapunov Risk=', 6.516273021697998)\n",
      "(203, 'Lyapunov Risk=', 6.486845016479492)\n",
      "(204, 'Lyapunov Risk=', 6.437252044677734)\n",
      "(205, 'Lyapunov Risk=', 6.39865779876709)\n",
      "(206, 'Lyapunov Risk=', 6.357495307922363)\n",
      "(207, 'Lyapunov Risk=', 6.313929557800293)\n",
      "(208, 'Lyapunov Risk=', 6.270162582397461)\n",
      "(209, 'Lyapunov Risk=', 6.22947883605957)\n",
      "(210, 'Lyapunov Risk=', 6.187536239624023)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-5.364257812500000888, -5.363434878877717971]\n",
      "x2 : [0, 0.001080982044006452642]\n",
      "==============================\n",
      "(211, 'Lyapunov Risk=', 6.077889919281006)\n",
      "(212, 'Lyapunov Risk=', 6.025279521942139)\n",
      "(213, 'Lyapunov Risk=', 5.990044116973877)\n",
      "(214, 'Lyapunov Risk=', 5.952033519744873)\n",
      "(215, 'Lyapunov Risk=', 5.91024923324585)\n",
      "(216, 'Lyapunov Risk=', 5.877894878387451)\n",
      "(217, 'Lyapunov Risk=', 5.833444595336914)\n",
      "(218, 'Lyapunov Risk=', 5.797731399536133)\n",
      "(219, 'Lyapunov Risk=', 5.760929107666016)\n",
      "(220, 'Lyapunov Risk=', 5.72365140914917)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.2128976090910684738, -0.2028976090910684649]\n",
      "x2 : [0.5106203499736460261, 0.5206203499736460349]\n",
      "==============================\n",
      "(221, 'Lyapunov Risk=', 5.755442142486572)\n",
      "(222, 'Lyapunov Risk=', 5.715060710906982)\n",
      "(223, 'Lyapunov Risk=', 5.67584228515625)\n",
      "(224, 'Lyapunov Risk=', 5.637060642242432)\n",
      "(225, 'Lyapunov Risk=', 5.599819660186768)\n",
      "(226, 'Lyapunov Risk=', 5.560527801513672)\n",
      "(227, 'Lyapunov Risk=', 5.520296096801758)\n",
      "(228, 'Lyapunov Risk=', 5.482691287994385)\n",
      "(229, 'Lyapunov Risk=', 5.445316314697266)\n",
      "(230, 'Lyapunov Risk=', 5.406836032867432)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-1.516718750000000338, -1.506718750000000551]\n",
      "x2 : [3.016949023588368917, 3.026949023588368703]\n",
      "==============================\n",
      "(231, 'Lyapunov Risk=', 5.302189350128174)\n",
      "(232, 'Lyapunov Risk=', 5.264694690704346)\n",
      "(233, 'Lyapunov Risk=', 5.231466770172119)\n",
      "(234, 'Lyapunov Risk=', 5.199121952056885)\n",
      "(235, 'Lyapunov Risk=', 5.166618347167969)\n",
      "(236, 'Lyapunov Risk=', 5.133851051330566)\n",
      "(237, 'Lyapunov Risk=', 5.110437393188477)\n",
      "(238, 'Lyapunov Risk=', 5.071399211883545)\n",
      "(239, 'Lyapunov Risk=', 5.040600299835205)\n",
      "(240, 'Lyapunov Risk=', 5.009028911590576)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.2161376037308062881, -0.2061376037308062792]\n",
      "x2 : [0.510324678957570943, 0.5203246789575709519]\n",
      "==============================\n",
      "(241, 'Lyapunov Risk=', 5.021634101867676)\n",
      "(242, 'Lyapunov Risk=', 4.991800785064697)\n",
      "(243, 'Lyapunov Risk=', 4.961135387420654)\n",
      "(244, 'Lyapunov Risk=', 4.930665969848633)\n",
      "(245, 'Lyapunov Risk=', 4.901123046875)\n",
      "(246, 'Lyapunov Risk=', 4.871495723724365)\n",
      "(247, 'Lyapunov Risk=', 4.842970371246338)\n",
      "(248, 'Lyapunov Risk=', 4.816355228424072)\n",
      "(249, 'Lyapunov Risk=', 4.792296409606934)\n",
      "(250, 'Lyapunov Risk=', 4.765382766723633)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.1513726739446581704, -0.1498612540866893494]\n",
      "x2 : [0.476535742188184841, 0.4783623632870440678]\n",
      "==============================\n",
      "(251, 'Lyapunov Risk=', 4.763029098510742)\n",
      "(252, 'Lyapunov Risk=', 4.747488498687744)\n",
      "(253, 'Lyapunov Risk=', 4.709361553192139)\n",
      "(254, 'Lyapunov Risk=', 4.682032585144043)\n",
      "(255, 'Lyapunov Risk=', 4.660506725311279)\n",
      "(256, 'Lyapunov Risk=', 4.638678550720215)\n",
      "(257, 'Lyapunov Risk=', 4.609723091125488)\n",
      "(258, 'Lyapunov Risk=', 4.583683013916016)\n",
      "(259, 'Lyapunov Risk=', 4.569421291351318)\n",
      "(260, 'Lyapunov Risk=', 4.541794776916504)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-1.049433279719221623, -1.048788640001165673]\n",
      "x2 : [3.002929687500000888, 3.003662109375000888]\n",
      "==============================\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(261, 'Lyapunov Risk=', 4.467488765716553)\n",
      "(262, 'Lyapunov Risk=', 4.453447341918945)\n",
      "(263, 'Lyapunov Risk=', 4.433908462524414)\n",
      "(264, 'Lyapunov Risk=', 4.4193010330200195)\n",
      "(265, 'Lyapunov Risk=', 4.385159492492676)\n",
      "(266, 'Lyapunov Risk=', 4.366495609283447)\n",
      "(267, 'Lyapunov Risk=', 4.351430892944336)\n",
      "(268, 'Lyapunov Risk=', 4.331546306610107)\n",
      "(269, 'Lyapunov Risk=', 4.3113322257995605)\n",
      "(270, 'Lyapunov Risk=', 4.292080879211426)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.1859291768294853431, -0.1759291768294853342]\n",
      "x2 : [0.4873300497552505162, 0.497330049755250525]\n",
      "==============================\n",
      "(271, 'Lyapunov Risk=', 4.2786478996276855)\n",
      "(272, 'Lyapunov Risk=', 4.25656795501709)\n",
      "(273, 'Lyapunov Risk=', 4.236761569976807)\n",
      "(274, 'Lyapunov Risk=', 4.219507217407227)\n",
      "(275, 'Lyapunov Risk=', 4.212627410888672)\n",
      "(276, 'Lyapunov Risk=', 4.18997859954834)\n",
      "(277, 'Lyapunov Risk=', 4.172178268432617)\n",
      "(278, 'Lyapunov Risk=', 4.160102844238281)\n",
      "(279, 'Lyapunov Risk=', 4.143537998199463)\n",
      "(280, 'Lyapunov Risk=', 4.134834289550781)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-2.829218750000000338, -2.819218750000000551]\n",
      "x2 : [5.198202879833448975, 5.208202879833448762]\n",
      "==============================\n",
      "(281, 'Lyapunov Risk=', 4.119067192077637)\n",
      "(282, 'Lyapunov Risk=', 4.085021495819092)\n",
      "(283, 'Lyapunov Risk=', 4.07386589050293)\n",
      "(284, 'Lyapunov Risk=', 4.060941219329834)\n",
      "(285, 'Lyapunov Risk=', 4.040304660797119)\n",
      "(286, 'Lyapunov Risk=', 4.037257671356201)\n",
      "(287, 'Lyapunov Risk=', 4.027769088745117)\n",
      "(288, 'Lyapunov Risk=', 3.9966185092926025)\n",
      "(289, 'Lyapunov Risk=', 3.9877734184265137)\n",
      "(290, 'Lyapunov Risk=', 3.979862928390503)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.1875000000000000278, -0.1846080407775102517]\n",
      "x2 : [0.4881659199228978174, 0.490407148511935953]\n",
      "==============================\n",
      "(291, 'Lyapunov Risk=', 3.962630033493042)\n",
      "(292, 'Lyapunov Risk=', 3.9544897079467773)\n",
      "(293, 'Lyapunov Risk=', 3.940854787826538)\n",
      "(294, 'Lyapunov Risk=', 3.922623872756958)\n",
      "(295, 'Lyapunov Risk=', 3.908928155899048)\n",
      "(296, 'Lyapunov Risk=', 3.8961739540100098)\n",
      "(297, 'Lyapunov Risk=', 3.8851206302642822)\n",
      "(298, 'Lyapunov Risk=', 3.8801629543304443)\n",
      "(299, 'Lyapunov Risk=', 3.864096164703369)\n",
      "(300, 'Lyapunov Risk=', 3.8525466918945312)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.2536612705891468922, -0.2516389584322993311]\n",
      "x2 : [0.4332086559021638417, 0.4355391854123052964]\n",
      "==============================\n",
      "(301, 'Lyapunov Risk=', 3.834986448287964)\n",
      "(302, 'Lyapunov Risk=', 3.8272488117218018)\n",
      "(303, 'Lyapunov Risk=', 3.8166871070861816)\n",
      "(304, 'Lyapunov Risk=', 3.8049299716949463)\n",
      "(305, 'Lyapunov Risk=', 3.7959930896759033)\n",
      "(306, 'Lyapunov Risk=', 3.781355142593384)\n",
      "(307, 'Lyapunov Risk=', 3.7772862911224365)\n",
      "(308, 'Lyapunov Risk=', 3.7736189365386963)\n",
      "(309, 'Lyapunov Risk=', 3.7572824954986572)\n",
      "(310, 'Lyapunov Risk=', 3.754567861557007)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-2.531982421875000444, -2.531250000000000444]\n",
      "x2 : [5.42339150050285479, 5.424364002158657883]\n",
      "==============================\n",
      "(311, 'Lyapunov Risk=', 3.743675470352173)\n",
      "(312, 'Lyapunov Risk=', 3.7314610481262207)\n",
      "(313, 'Lyapunov Risk=', 3.7252509593963623)\n",
      "(314, 'Lyapunov Risk=', 3.7125535011291504)\n",
      "(315, 'Lyapunov Risk=', 3.7017087936401367)\n",
      "(316, 'Lyapunov Risk=', 3.6941049098968506)\n",
      "(317, 'Lyapunov Risk=', 3.689378023147583)\n",
      "(318, 'Lyapunov Risk=', 3.679091453552246)\n",
      "(319, 'Lyapunov Risk=', 3.671111822128296)\n",
      "(320, 'Lyapunov Risk=', 3.6610605716705322)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-3.001464843750000888, -3.000000000000000444]\n",
      "x2 : [1.225617554473976689, 1.227195989973271395]\n",
      "==============================\n",
      "(321, 'Lyapunov Risk=', 3.714641809463501)\n",
      "(322, 'Lyapunov Risk=', 3.7049474716186523)\n",
      "(323, 'Lyapunov Risk=', 3.697598457336426)\n",
      "(324, 'Lyapunov Risk=', 3.693079710006714)\n",
      "(325, 'Lyapunov Risk=', 3.6840596199035645)\n",
      "(326, 'Lyapunov Risk=', 3.679558277130127)\n",
      "(327, 'Lyapunov Risk=', 3.674119710922241)\n",
      "(328, 'Lyapunov Risk=', 3.6678919792175293)\n",
      "(329, 'Lyapunov Risk=', 3.6624865531921387)\n",
      "(330, 'Lyapunov Risk=', 3.6563384532928467)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [5.718754797704725945, 5.719289895222012809]\n",
      "x2 : [1.813759381619124644, 1.814780627491174414]\n",
      "==============================\n",
      "(331, 'Lyapunov Risk=', 3.631375312805176)\n",
      "(332, 'Lyapunov Risk=', 3.6143107414245605)\n",
      "(333, 'Lyapunov Risk=', 3.613492965698242)\n",
      "(334, 'Lyapunov Risk=', 3.6118476390838623)\n",
      "(335, 'Lyapunov Risk=', 3.609877586364746)\n",
      "(336, 'Lyapunov Risk=', 3.6061151027679443)\n",
      "(337, 'Lyapunov Risk=', 3.6014397144317627)\n",
      "(338, 'Lyapunov Risk=', 3.5957865715026855)\n",
      "(339, 'Lyapunov Risk=', 3.5902955532073975)\n",
      "(340, 'Lyapunov Risk=', 3.5876150131225586)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-2.261718750000000444, -2.260986328125000444]\n",
      "x2 : [5.108904769987626437, 5.110035054514644237]\n",
      "==============================\n",
      "(341, 'Lyapunov Risk=', 3.5630898475646973)\n",
      "(342, 'Lyapunov Risk=', 3.5584967136383057)\n",
      "(343, 'Lyapunov Risk=', 3.553330898284912)\n",
      "(344, 'Lyapunov Risk=', 3.5476765632629395)\n",
      "(345, 'Lyapunov Risk=', 3.540334463119507)\n",
      "(346, 'Lyapunov Risk=', 3.531574249267578)\n",
      "(347, 'Lyapunov Risk=', 3.523676872253418)\n",
      "(348, 'Lyapunov Risk=', 3.520909070968628)\n",
      "(349, 'Lyapunov Risk=', 3.5178892612457275)\n",
      "(350, 'Lyapunov Risk=', 3.513444185256958)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [3.112485192541876167, 3.112567414496483664]\n",
      "x2 : [-5.129564886635860965, -5.129436343532018938]\n",
      "==============================\n",
      "(351, 'Lyapunov Risk=', 3.5391128063201904)\n",
      "(352, 'Lyapunov Risk=', 3.535552501678467)\n",
      "(353, 'Lyapunov Risk=', 3.5304532051086426)\n",
      "(354, 'Lyapunov Risk=', 3.5208303928375244)\n",
      "(355, 'Lyapunov Risk=', 3.519991874694824)\n",
      "(356, 'Lyapunov Risk=', 3.5132744312286377)\n",
      "(357, 'Lyapunov Risk=', 3.5109126567840576)\n",
      "(358, 'Lyapunov Risk=', 3.5104048252105713)\n",
      "(359, 'Lyapunov Risk=', 3.5026707649230957)\n",
      "(360, 'Lyapunov Risk=', 3.5006349086761475)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [2.812500000000000444, 2.81662559707897131]\n",
      "x2 : [-5.196289852720591185, -5.189376825607732613]\n",
      "==============================\n",
      "(361, 'Lyapunov Risk=', 3.524181365966797)\n",
      "(362, 'Lyapunov Risk=', 3.5231637954711914)\n",
      "(363, 'Lyapunov Risk=', 3.5160486698150635)\n",
      "(364, 'Lyapunov Risk=', 3.5099103450775146)\n",
      "(365, 'Lyapunov Risk=', 3.504572868347168)\n",
      "(366, 'Lyapunov Risk=', 3.5018677711486816)\n",
      "(367, 'Lyapunov Risk=', 3.496192455291748)\n",
      "(368, 'Lyapunov Risk=', 3.4946627616882324)\n",
      "(369, 'Lyapunov Risk=', 3.491049289703369)\n",
      "(370, 'Lyapunov Risk=', 3.485170364379883)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-3.026756108625401787, -3.016756108625402]\n",
      "x2 : [1.604040080969925341, 1.614040080969925128]\n",
      "==============================\n",
      "(371, 'Lyapunov Risk=', 3.5362939834594727)\n",
      "(372, 'Lyapunov Risk=', 3.5202348232269287)\n",
      "(373, 'Lyapunov Risk=', 3.5221378803253174)\n",
      "(374, 'Lyapunov Risk=', 3.5201358795166016)\n",
      "(375, 'Lyapunov Risk=', 3.512338161468506)\n",
      "(376, 'Lyapunov Risk=', 3.5143465995788574)\n",
      "(377, 'Lyapunov Risk=', 3.5137338638305664)\n",
      "(378, 'Lyapunov Risk=', 3.5072343349456787)\n",
      "(379, 'Lyapunov Risk=', 3.497779130935669)\n",
      "(380, 'Lyapunov Risk=', 3.4986822605133057)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [2.656510359395632292, 2.658411076737418277]\n",
      "x2 : [-5.306796796088629087, -5.30541377003178205]\n",
      "==============================\n",
      "(381, 'Lyapunov Risk=', 3.51435923576355)\n",
      "(382, 'Lyapunov Risk=', 3.512869358062744)\n",
      "(383, 'Lyapunov Risk=', 3.5111119747161865)\n",
      "(384, 'Lyapunov Risk=', 3.5091211795806885)\n",
      "(385, 'Lyapunov Risk=', 3.50913405418396)\n",
      "(386, 'Lyapunov Risk=', 3.5056252479553223)\n",
      "(387, 'Lyapunov Risk=', 3.498361825942993)\n",
      "(388, 'Lyapunov Risk=', 3.494896650314331)\n",
      "(389, 'Lyapunov Risk=', 3.494188070297241)\n",
      "(390, 'Lyapunov Risk=', 3.4923524856567383)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [2.64856724804924637, 2.650380113283803851]\n",
      "x2 : [-5.3191320085043996, -5.317941720141549311]\n",
      "==============================\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(391, 'Lyapunov Risk=', 3.5057055950164795)\n",
      "(392, 'Lyapunov Risk=', 3.501476526260376)\n",
      "(393, 'Lyapunov Risk=', 3.4977786540985107)\n",
      "(394, 'Lyapunov Risk=', 3.493021011352539)\n",
      "(395, 'Lyapunov Risk=', 3.488341808319092)\n",
      "(396, 'Lyapunov Risk=', 3.482726812362671)\n",
      "(397, 'Lyapunov Risk=', 3.4778950214385986)\n",
      "(398, 'Lyapunov Risk=', 3.475555419921875)\n",
      "(399, 'Lyapunov Risk=', 3.475456714630127)\n",
      "(400, 'Lyapunov Risk=', 3.4726316928863525)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [5.84309023019527185, 5.84443130150275536]\n",
      "x2 : [0.9539811088562959451, 0.9565182926564457233]\n",
      "==============================\n",
      "(401, 'Lyapunov Risk=', 3.4373764991760254)\n",
      "(402, 'Lyapunov Risk=', 3.4305500984191895)\n",
      "(403, 'Lyapunov Risk=', 3.424783945083618)\n",
      "(404, 'Lyapunov Risk=', 3.423220634460449)\n",
      "(405, 'Lyapunov Risk=', 3.4226341247558594)\n",
      "(406, 'Lyapunov Risk=', 3.4207546710968018)\n",
      "(407, 'Lyapunov Risk=', 3.418185234069824)\n",
      "(408, 'Lyapunov Risk=', 3.415347099304199)\n",
      "(409, 'Lyapunov Risk=', 3.4133541584014893)\n",
      "(410, 'Lyapunov Risk=', 3.4080710411071777)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.09667968750000002776, -0.09375000000000001388]\n",
      "x2 : [0.6451797284707685431, 0.6484553619560570192]\n",
      "==============================\n",
      "(411, 'Lyapunov Risk=', 3.378236770629883)\n",
      "(412, 'Lyapunov Risk=', 3.3780176639556885)\n",
      "(413, 'Lyapunov Risk=', 3.3755111694335938)\n",
      "(414, 'Lyapunov Risk=', 3.373756170272827)\n",
      "(415, 'Lyapunov Risk=', 3.3727505207061768)\n",
      "(416, 'Lyapunov Risk=', 3.3675413131713867)\n",
      "(417, 'Lyapunov Risk=', 3.3648500442504883)\n",
      "(418, 'Lyapunov Risk=', 3.361788034439087)\n",
      "(419, 'Lyapunov Risk=', 3.361541748046875)\n",
      "(420, 'Lyapunov Risk=', 3.360348701477051)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-0.1021261518600057039, -0.09375000000000001388]\n",
      "x2 : [0.4894591393633047627, 0.4946254940542693657]\n",
      "==============================\n",
      "(421, 'Lyapunov Risk=', 3.3366246223449707)\n",
      "(422, 'Lyapunov Risk=', 3.3338088989257812)\n",
      "(423, 'Lyapunov Risk=', 3.332364559173584)\n",
      "(424, 'Lyapunov Risk=', 3.330303192138672)\n",
      "(425, 'Lyapunov Risk=', 3.330233573913574)\n",
      "(426, 'Lyapunov Risk=', 3.3284401893615723)\n",
      "(427, 'Lyapunov Risk=', 3.3239245414733887)\n",
      "(428, 'Lyapunov Risk=', 3.326178550720215)\n",
      "(429, 'Lyapunov Risk=', 3.3261027336120605)\n",
      "(430, 'Lyapunov Risk=', 3.321793794631958)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [-2.252929687500000444, -2.250000000000000444]\n",
      "x2 : [3.000000000000000444, 3.002743627948546212]\n",
      "==============================\n",
      "(431, 'Lyapunov Risk=', 3.3283896446228027)\n",
      "(432, 'Lyapunov Risk=', 3.3259940147399902)\n",
      "(433, 'Lyapunov Risk=', 3.3203349113464355)\n",
      "(434, 'Lyapunov Risk=', 3.3190174102783203)\n",
      "(435, 'Lyapunov Risk=', 3.3182790279388428)\n",
      "(436, 'Lyapunov Risk=', 3.3164076805114746)\n",
      "(437, 'Lyapunov Risk=', 3.3130836486816406)\n",
      "(438, 'Lyapunov Risk=', 3.309739589691162)\n",
      "(439, 'Lyapunov Risk=', 3.308321237564087)\n",
      "(440, 'Lyapunov Risk=', 3.3051934242248535)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [2.250000000000000444, 2.251387593431035228]\n",
      "x2 : [-5.055781397217791628, -5.053520828163756917]\n",
      "==============================\n",
      "(441, 'Lyapunov Risk=', 3.298685073852539)\n",
      "(442, 'Lyapunov Risk=', 3.295581817626953)\n",
      "(443, 'Lyapunov Risk=', 3.2932660579681396)\n",
      "(444, 'Lyapunov Risk=', 3.290825128555298)\n",
      "(445, 'Lyapunov Risk=', 3.289808750152588)\n",
      "(446, 'Lyapunov Risk=', 3.2902019023895264)\n",
      "(447, 'Lyapunov Risk=', 3.285721778869629)\n",
      "(448, 'Lyapunov Risk=', 3.291517972946167)\n",
      "(449, 'Lyapunov Risk=', 3.2856056690216064)\n",
      "(450, 'Lyapunov Risk=', 3.288159132003784)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [0.1733918658537869639, 0.1750353411762177458]\n",
      "x2 : [-0.4840585740285081595, -0.4817756664079493323]\n",
      "==============================\n",
      "(451, 'Lyapunov Risk=', 3.2653183937072754)\n",
      "(452, 'Lyapunov Risk=', 3.2587270736694336)\n",
      "(453, 'Lyapunov Risk=', 3.2618229389190674)\n",
      "(454, 'Lyapunov Risk=', 3.2626144886016846)\n",
      "(455, 'Lyapunov Risk=', 3.256481409072876)\n",
      "(456, 'Lyapunov Risk=', 3.2548952102661133)\n",
      "(457, 'Lyapunov Risk=', 3.257826328277588)\n",
      "(458, 'Lyapunov Risk=', 3.248716115951538)\n",
      "(459, 'Lyapunov Risk=', 3.247966766357422)\n",
      "(460, 'Lyapunov Risk=', 3.2491605281829834)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [0.1794344902678468856, 0.181287312267032652]\n",
      "x2 : [-0.4799520931785536959, -0.476664155631538744]\n",
      "==============================\n",
      "(461, 'Lyapunov Risk=', 3.2225749492645264)\n",
      "(462, 'Lyapunov Risk=', 3.2251532077789307)\n",
      "(463, 'Lyapunov Risk=', 3.2242555618286133)\n",
      "(464, 'Lyapunov Risk=', 3.2173807621002197)\n",
      "(465, 'Lyapunov Risk=', 3.2183637619018555)\n",
      "(466, 'Lyapunov Risk=', 3.21889591217041)\n",
      "(467, 'Lyapunov Risk=', 3.2165443897247314)\n",
      "(468, 'Lyapunov Risk=', 3.2141692638397217)\n",
      "(469, 'Lyapunov Risk=', 3.2108242511749268)\n",
      "(470, 'Lyapunov Risk=', 3.2103660106658936)\n",
      "===========Verifying==========\n",
      "Not a Lyapunov function. Found counterexample: \n",
      "x1 : [0.750000000000000111, 0.7511178612164770563]\n",
      "x2 : [-1.501464843750000444, -1.500000000000000222]\n",
      "==============================\n",
      "(471, 'Lyapunov Risk=', 3.1852200031280518)\n",
      "(472, 'Lyapunov Risk=', 3.184959650039673)\n",
      "(473, 'Lyapunov Risk=', 3.182744264602661)\n",
      "(474, 'Lyapunov Risk=', 3.1796915531158447)\n",
      "(475, 'Lyapunov Risk=', 3.178271532058716)\n",
      "(476, 'Lyapunov Risk=', 3.176910638809204)\n",
      "(477, 'Lyapunov Risk=', 3.17410945892334)\n",
      "(478, 'Lyapunov Risk=', 3.1730144023895264)\n",
      "(479, 'Lyapunov Risk=', 3.171429395675659)\n",
      "(480, 'Lyapunov Risk=', 3.1702136993408203)\n",
      "===========Verifying==========\n",
      "Satisfy conditions!!\n",
      "(<Expression \"tanh((0.49927884340286255 - 0.41210386157035828 * tanh((-0.79895162582397461 - 0.053098957985639572 * x1 + 0.046276744455099106 * x2)) + 0.82691246271133423 * tanh((-0.6677706241607666 + 0.69698750972747803 * x1 - 0.0021623193752020597 * x2)) - 0.9570583701133728 * tanh((0.83614975214004517 + 0.9072798490524292 * x1 + 0.013366221450269222 * x2)) - 0.059784829616546631 * tanh((0.90165179967880249 + 0.16413372755050659 * x1 - 0.36351147294044495 * x2)) + 0.97691076993942261 * tanh((1.1444443464279175 + 0.028182908892631531 * x1 - 0.026499949395656586 * x2)) - 0.27872595191001892 * tanh((1.3038069009780884 - 0.43813130259513855 * x1 - 0.24401682615280151 * x2))))\">, ' is a Lyapunov function.')\n",
      "==============================\n",
      "\n",
      "\n",
      "('Total time: ', 37.35398197174072)\n",
      "('Verified time: ', 1.0700631141662598)\n"
     ]
    }
   ],
   "source": [
    "out_iters = 0\n",
    "valid = False\n",
    "while out_iters < 2 and not valid: \n",
    "    start = timeit.default_timer()\n",
    "    lqr = torch.tensor([[-23.58639732,  -5.31421063]])    # lqr solution\n",
    "    model = Net(D_in,H1, D_out,lqr)\n",
    "    L = []\n",
    "    i = 0 \n",
    "    t = 0\n",
    "    max_iters = 2000\n",
    "    learning_rate = 0.01\n",
    "    optimizer = torch.optim.Adam(model.parameters(), lr=learning_rate)\n",
    "\n",
    "    while i < max_iters and not valid: \n",
    "        V_candidate, u = model(x)\n",
    "        X0,u0 = model(x_0)\n",
    "        f = f_value(x,u)\n",
    "        Circle_Tuning = Tune(x)\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",
    "        # With tuning term \n",
    "        Lyapunov_risk = (F.relu(-V_candidate)+ 1.5*F.relu(L_V+0.5)).mean()\\\n",
    "                    +2.2*((Circle_Tuning-6*V_candidate).pow(2)).mean()+(X0).pow(2) \n",
    "        # Without tuning term\n",
    "#         Lyapunov_risk = (F.relu(-V_candidate)+ 1.5*F.relu(L_V+0.5)).mean()+ 1.2*(X0).pow(2)\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",
    "        w1 = model.layer1.weight.data.numpy()\n",
    "        w2 = model.layer2.weight.data.numpy()\n",
    "        b1 = model.layer1.bias.data.numpy()\n",
    "        b2 = model.layer2.bias.data.numpy()\n",
    "        q = model.control.weight.data.numpy()\n",
    "\n",
    "        # Falsification\n",
    "        if i % 10 == 0:\n",
    "            u_NN = (q.item(0)*x1 + q.item(1)*x2) \n",
    "            f = [ x2,\n",
    "                 (m*G*l*sin(x1) + u_NN - b*x2) /(m*l**2)]\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",
    "            result= CheckLyapunov(vars_, f, V_learn, ball_lb, ball_ub, config,epsilon)\n",
    "            stop_ = timeit.default_timer() \n",
    "\n",
    "            if (result): \n",
    "                print(\"Not a Lyapunov function. Found counterexample: \")\n",
    "                print(result)\n",
    "                x = AddCounterexamples(x,result,10)\n",
    "            else:  \n",
    "                valid = True\n",
    "                print(\"Satisfy conditions!!\")\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",
    "\n",
    "    np.savetxt(\"w1.txt\", model.layer1.weight.data, fmt=\"%s\")\n",
    "    np.savetxt(\"w2.txt\", model.layer2.weight.data, fmt=\"%s\")\n",
    "    np.savetxt(\"b1.txt\", model.layer1.bias.data, fmt=\"%s\")\n",
    "    np.savetxt(\"b2.txt\", model.layer2.bias.data, fmt=\"%s\")\n",
    "    np.savetxt(\"q.txt\", model.control.weight.data, 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": {},
   "source": [
    "### Checking result with smaller epsilon ( Lie derivative of V <= epsilon )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "('Satisfy conditions with epsilon= ', -1e-05)\n",
      "(<Expression \"tanh((0.49927884340286255 - 0.41210386157035828 * tanh((-0.79895162582397461 - 0.053098957985639572 * x1 + 0.046276744455099106 * x2)) + 0.82691246271133423 * tanh((-0.6677706241607666 + 0.69698750972747803 * x1 - 0.0021623193752020597 * x2)) - 0.9570583701133728 * tanh((0.83614975214004517 + 0.9072798490524292 * x1 + 0.013366221450269222 * x2)) - 0.059784829616546631 * tanh((0.90165179967880249 + 0.16413372755050659 * x1 - 0.36351147294044495 * x2)) + 0.97691076993942261 * tanh((1.1444443464279175 + 0.028182908892631531 * x1 - 0.026499949395656586 * x2)) - 0.27872595191001892 * tanh((1.3038069009780884 - 0.43813130259513855 * x1 - 0.24401682615280151 * x2))))\">, ' is a Lyapunov function.')\n"
     ]
    }
   ],
   "source": [
    "epsilon = -0.00001\n",
    "start_ = timeit.default_timer() \n",
    "result = CheckLyapunov(vars_, f, V_learn, ball_lb, ball_ub, config, epsilon)\n",
    "stop_ = timeit.default_timer() \n",
    "\n",
    "if (result): \n",
    "    print(\"Not a Lyapunov function. Found counterexample: \")\n",
    "else:  \n",
    "    print(\"Satisfy conditions with epsilon= \",epsilon)\n",
    "    print(V_learn, \" is a Lyapunov function.\")\n",
    "t += (stop_ - start_)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### More details on Lyapunov risk\n",
    "Generally, we start training with Lyapunov risk without the tuning term.      \n",
    "For example, (1* F.relu(-V_candidate)+ 1.5* F.relu(L_V+0.5)).mean()+ 1.2*(X0).pow(2)    \n",
    "The weight of each term (1, 1.5, 1.2) can be tuned for balancing each Lyapunov condition.     \n",
    "Furthermore, using F.relu(L_V+0.5) allows the learning procedure to seek a candidate Lyapunov function with more negative Lie derivative.   \n",
    "Here 0.5 is also a tunable parameter based on your goal.    \n",
    "In this example, we use Lyapunov risk with tuning term for achieving large ROA     "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 2",
   "language": "python",
   "name": "python2"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 2
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython2",
   "version": "2.7.15"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}