fm-2019-tutorial.kyx

ArchiveEntry "FM19/1 Bouncing ball"
Description "Acrophobic Bouncing Ball".

Definitions       /* function symbols cannot change their value */
  Real H;         /* initial height */
  Real g;         /* gravity */
  Real c;         /* damping coefficient */
End.

ProgramVariables  /* program variables may change their value over time */
  Real x, v;      /* height and vertical velocity */
End.

Problem
  x>=0 & x=H
  & v=0 & g>0 & 1>=c&c>=0
 ->
  [
    {
      {x'=v,v'=-g&x>=0}
      if (x=0) {v:=-c*v;}
    }* @invariant(2*g*x<=2*g*H-v^2 & x>=0)
  ] (x>=0 & x<=H)
End.

Tactic "Bouncing Ball: Clever Proof"
implyR(1) ; loop("2*g*x<=2*g*H-v^2&x>=0", 1) ; <(
  QE,
  QE,
  composeb(1) ; dC("2*g*x<=2*g*H-v^2", 1) ; <(
    dW(1) ; choiceb(1) ; andR(1) ; <(
      composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; QE,
      composeb(1) ; testb(1) ; implyR(1) ; testb(1) ; implyR(1) ; prop ; done
      ),
    dI(1)
    )
  )
End.

Tactic "Bouncing Ball: automatic"
  useSolver("Mathematica");
  master
End.

Illustration "https://lfcps.org/info/fig-bouncing-ball-dark-trace.png".
End.
Exercise "FM19/2 Exercise: Runaround Robot"
Description "CurveBot: run a robot round the bend".

ProgramVariables
  Real x, y;    /* robot x/y position */
  Real v, w;    /* robot orientation in x/y direction */
  Real om;      /* robot rotational velocity */
  Real ox, oy;  /* x/y position summary of obstacle */
End.

Definitions
  Bool Q(Real om, Real x, Real y, Real ox, Real oy, Real v, Real w) <-> 
    (__________).
  Bool Qline(Real x, Real y, Real ox, Real oy, Real v, Real w) <-> 
    (__________).
End.
    
Problem
  x!=ox | y!=oy ->
  [{
    {?Q(-1,x,y,ox,oy,v,w); om:=-1;
    ++ ?Q(1,x,y,ox,oy,v,w); om:=1;
    ++ ?Qline(x,y,ox,oy,v,w); om:=0;}
    {x'=v,y'=w,v'=om*w,w'=-om*v}
   }*
  ] !(x=ox & y=oy)
End.

Illustration "https://lfcps.org/info/fig-Dubins-path-robotesque-1.png".
End.
/* Exported from KeYmaera X v4.7.4 */

ArchiveEntry "FM19/2 Solution: Runaround Robot"
Description "CurveBot: run a robot round the bend".

ProgramVariables
  Real x, y;    /* robot x/y position */
  Real v, w;    /* robot orientation in x/y direction */
  Real om;      /* robot rotational velocity */
  Real ox, oy;  /* x/y position summary of obstacle */
End.

Definitions
  Bool Q(Real om, Real x, Real y, Real ox, Real oy, Real v, Real w) <-> 
    ((x+w/om-ox)^2+(y-v/om-oy)^2 != v^2+w^2).
  Bool Qline(Real x, Real y, Real ox, Real oy, Real v, Real w) <-> 
    ((ox-x)*w != (oy-y)*v).
End.
    
Problem
  x!=ox | y!=oy ->
  [{
    {?Q(-1,x,y,ox,oy,v,w); om:=-1;
    ++ ?Q(1,x,y,ox,oy,v,w); om:=1;
    ++ ?Qline(x,y,ox,oy,v,w); om:=0;}
    {x'=v,y'=w,v'=om*w,w'=-om*v}
   }* @invariant(!(x=ox & y=oy))
  ] !(x=ox & y=oy)
End.


Tactic "4 Solution: Runaround Robot: Proof"
implyR(1) ; loop("!(x=ox&y=oy)", 1) ; <(
  QE,
  id,
  composeb(1) ; choiceb(1) ; andR(1) ; <(
    unfold ; expand "Q" ; ODE(1),
    unfold ; <(
      expand "Q" ; ODE(1),
      expand "Qline" ; ODE(1)
      )
    )
  )
End.


Tactic "4 Solution: Runaround Robot: Manual Proof"
  implyR(1) ; loop("!(x=ox&y=oy)", 1) ; <(
  QE,
  id,
  composeb(1) ; choiceb(1) ; andR(1) ; <(
    composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; dC("v=-1*(y-old(y-v/-1))&w=1*(x-old(x+w/-1))", 1) ; <(
      dC("(x+w/-1-ox)^2+(y-v/-1-oy)^2!=v^2+w^2", 1) ; <(
        dW(1) ; QE,
        dI(1)
        ),
      dI(1)
      ),
    choiceb(1) ; andR(1) ; <(
      composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; dC("v=1*(y-old(y-v/1))&w=-1*(x-old(x+w/1))", 1) ; <(
        dC("(x+w/1-ox)^2+(y-v/1-oy)^2!=v^2+w^2", 1) ; <(
          dW(1) ; QE,
          dI(1)
          ),
        dI(1)
        ),
      composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; dG("t'=1", "!(x=ox&y=oy)", 1) ; existsR("0", 1) ; dC("v=old(v)&w=old(w)&x=old(x)+v*t&y=old(y)+w*t", 1) ; <(
        dW(1) ; QE,
        dI(1)
        )
      )
    )
  )
End.

Tactic "4 Solution: Runaround Robot: automatic"
  master
End.

Tactic "4 Solution: Runaround Robot: unfold"
unfold ; loop("!(x=ox&y=oy)", 1) ; <(
  QE,
  QE,
  unfold ; doall(ODE(1))
  )
End.


Illustration "https://lfcps.org/info/fig-Dubins-path-robotesque-1.png".

End.ArchiveEntry "FM19/3 Swirl invariant"
Description "LICS'18 hourglass swirl".

ProgramVariables
  Real u;
  Real v;
End.

Problem
  u^2<=v^2+9/2 -> [{u'=-v+u/4*(1-u^2-v^2),v'=u+v/4*(1-u^2-v^2)}]u^2<=v^2+9/2
End.
Tactic "Swirl invariant: Proof"
master
End.

Illustration "https://lfcps.org/info/fig-invariant-swirl-example.png".
End.

ArchiveEntry "FM19/3 Swirl invariant circle"
Description "LICS'18 circle swirl".

ProgramVariables
  Real u;
  Real v;
End.

Problem
  u^2+v^2=1 -> [{u'=-v+u/4*(1-u^2-v^2),v'=u+v/4*(1-u^2-v^2)}]u^2+v^2=1
End.
Tactic "Swirl invariant circle: Proof"
master
End.
Illustration "https://lfcps.org/info/fig-invariant-swirl-example.png".
End.

ArchiveEntry "FM19/3 Swirl invariant disc"
Description "LICS'18 disc swirl".

ProgramVariables
  Real u;
  Real v;
End.

Problem
  1-u^2-v^2>0 -> [{u'=-v+u/4*(1-u^2-v^2),v'=u+v/4*(1-u^2-v^2)}]1-u^2-v^2>0
End.
Tactic "Swirl invariant disc: Proof"
master
End.
Illustration "https://lfcps.org/info/fig-invariant-swirl-example.png".
End.
ArchiveEntry "FM19/4 Damped oscillator"
Description "Damped oscillators stay in ellipses".

Definitions        /* function symbols cannot change their value */
  Real w;          /* undamped angular frequency */
  Real c;          /* level of ellipse */
  Real d;          /* constant damping ratio */
End.

ProgramVariables  /* program variables may change their value over time */
  Real x;         /* position of spring/mass system */
  Real y;         /* velocity */
End.

Problem
    w^2*x^2 + y^2 <= c^2
->
  [{x'=y, y'=-w^2*x-2*d*w*y & w>=0 & d>=0}]w^2*x^2 + y^2 <= c^2
End.

Tactic "Damped Oscillator: Differential invariant proof"
  implyR(1) ; dI(1)
End.

Tactic "Damped Oscillator: automatic"
  master
End.

Illustration "https://lfcps.org/info/fig-damposc-evo2t-region.png".
End.


ArchiveEntry "FM19/4 Increasingly damped oscillator"
Description "Increasingly damped oscillators stay in ellipses".

Definitions
  Real w;    /* undamped angular frequency */
  Real c;    /* level of ellipse */
End.

ProgramVariables
  Real x;    /* position of spring/mass system */
  Real y;    /* velocity */
  Real d;    /* damping ratio */
End.

Problem
    w^2*x^2 + y^2 <= c^2
  & d>=0
->
  [{x'=y, y'=-w^2*x-2*d*w*y, d'=7 & w>=0}]w^2*x^2 + y^2 <= c^2
End.

Tactic "Increasingly Damped Oscillator: Differential cut proof"
  implyR(1) ; dC("d>=0", 1) ; <(
    dI(1), 
    dI(1)
  )
End.

Tactic "Increasingly Damped Oscillator: automatic"
  master
End.

Illustration "https://lfcps.org/info/fig-damped-damped-osc-field-region.png".
End.
ArchiveEntry "FM19/5 Kepler two body"
Description "Two planets in gravitational force field with one planet as origin, mathematically normalized constants".
Citation "Ernst Hairer. Geometric Numerical Integration. TU Munich 2010".

Definitions
  Real e;        /* eccentricity */
  Real E;        /* generalized energy level */
End.

ProgramVariables
  Real x,y;      /* x/y coordinates of the planet */
  Real v,w;      /* x/y velocities of the planet */
End.

Problem
  /* 0<=e&e<1 &
  x=1-e&v=0 & y=0&w=((1+e)/(1-e))^(1/2) & */
  (v^2+w^2)/2-1/(x^2+y^2)^(1/2) = E ->
   [{x'=v,v'=-x/(x^2+y^2)^(3/2),
     y'=w,w'=-y/(x^2+y^2)^(3/2)&(x!=0|y!=0)}] (v^2+w^2)/2-1/(x^2+y^2)^(1/2) = E
End.

Tactic "Kepler two body: Proof"
useSolver("Mathematica");
implyR(1) ; dI(1)
End.

Tactic "Kepler two body: Proof"
useSolver("Mathematica");
master
End.

Illustration "https://lfcps.org/info/Kepler.png".
End.
ArchiveEntry "FM19/6 Coasting Car"
Description "Coasting cars can stop".

Definitions       /* function symbols cannot change their value */
  Real b;         /* braking capabilities */
  Real ep;        /* reaction time */
End.

ProgramVariables  /* program variables may change their value over time */
  Real x;         /* position of the car */
  Real v;         /* velocity of the car */
  Real a;         /* acceleration of the car */
  Real m;         /* stop sign position */
  Real t;         /* clock variable */
End.

Problem           /* differential dynamic logic formula */
    v^2<=2*b*(m-x) & v>=0  & b>0
 -> [
      {
        {a:=-b; ++ ?v^2<=2*b*(m-x-ep*v); a:=0;}
        t := 0;
        {x'=v, v'=a, t'=1 & v>=0 & t<=ep}
      }*@invariant(v^2<=2*b*(m-x))
    ] x <= m
End.
Tactic "Coasting Car: Interactive Proof"
implyR(1) ; loop("v^2<=2*b*(m-x)", 1) ; <(
  prop,
  QE,
  composeb(1) ; composeb(1.1) ; choiceb(1) ; andR(1) ; <(
    assignb(1) ; assignb(1) ; solve(1) ; QE,
    composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; assignb(1) ; solve(1) ; QE
    )
  )
End.

Tactic "Coasting Car: Automatic Proof"
  master
End.

End.ArchiveEntry "FM19/7 Exercise: Accelerating Car"
Description "Cars need invariants and control constraints to stop before m".

Definitions       /* function symbols cannot change their value */
  Real b;         /* braking capabilities */
  Real A;         /* maximum acceleration */
  Real ep;        /* reaction time */
End.

ProgramVariables  /* program variables may change their value over time */
  Real x;         /* position of the car */
  Real v;         /* velocity of the car */
  Real a;         /* acceleration of the car */
  Real m;         /* stop sign position */
  Real t;         /* clock variable */
End.

Problem           /* differential dynamic logic formula */
    v^2<=2*b*(m-x) & v>=0  & A>=0 & b>0
 -> [
      {
        {a:=-b; ++ ?__________; a:=A;}
        t := 0;
        {x'=v, v'=a, t'=1 & v>=0 & t<=ep}
      }* @invariant(__________)
    ] x <= m
End.

End.ArchiveEntry "FM19/7 Solution: Accelerating Car"
Description "Cars don't run stop signs".

Definitions       /* function symbols cannot change their value */
  Real b;         /* braking capabilities */
  Real A;         /* maximum acceleration */
  Real ep;        /* reaction time */
End.

ProgramVariables  /* program variables may change their value over time */
  Real x;         /* position of the car */
  Real v;         /* velocity of the car */
  Real a;         /* acceleration of the car */
  Real m;         /* stop sign position */
  Real t;         /* clock variable */
End.

Problem           /* differential dynamic logic formula */
    v^2<=2*b*(m-x) & v>=0  & A>=0 & b>0
 -> [
      {
        {a:=-b; ++ ?(2*b*(m-x) >= v^2+(A+b)*(A*ep^2+2*ep*v)); a:=A;}
        t := 0;
        {x'=v, v'=a, t'=1 & v>=0 & t<=ep}
      }*@invariant(v^2<=2*b*(m-x))
    ] x <= m
End.

Tactic "Safety of time-triggered car: Clever Proof"
implyR(1) ; loop("v^2<=2*b*(m-x)", 1) ; <(
  id,
  QE,
  composeb(1) ; choiceb(1) ; andR(1) ; <(
    assignb(1) ; composeb(1) ; assignb(1) ; dI(1)
    ,
    composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; composeb(1) ; assignb(1) ; dC("2*b*(m-x)>=v^2+(A+b)*(A*(ep-t)^2+2*(ep-t)*v)", 1) ; <(
      dW(1) ; QE,
      dI(1)
      )
    )
  )
End.

Tactic "Safety of time-triggered car: Interactive Proof"
  implyR(1) ; loop("v^2<=2*b*(m-x)", 1) ; <(
  QE,
  QE,
  composeb(1) ; choiceb(1) ; andR(1) ; <(
    assignb(1) ; composeb(1) ; assignb(1) ; solveEnd(1) ; QE
    ,
    composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; composeb(1) ; assignb(1) ; solveEnd(1) ; QE
    )
  )
End.
       
Tactic "Safety of time-triggered car: Automatic"
  master
End.

End.
ArchiveEntry "FM19/8 01 Exercise: Speed Control Loop Invariant"
Description "Find a Loop Invariant for Braking".

Definitions       /* function symbols cannot change their value */
  Real D;         /* speed limit sign position */
  Real S;         /* posted speed limit */
  Real B;         /* brakes */
  Real ep;
  Real A;
End.

ProgramVariables  /* program variables may change their value over time */
  Real x, v, a;   /* car position, speed, and acceleration */
  Real t;         /* time */
End.

Problem
  x<=D & S>=0 & B>0 & __________
 ->
  [
    {
      { a := -B; }
      {x'=v, v'=a & v>=0}
    }*@invariant(__________)
  ](x>=D -> v<=S)
End.

Tactic "Speed Control: Explore"
  explore
End.

Tactic "Speed Control: Solution"
  implyR(1) ; loop("v^2-S^2<=2*B*(D-x)", 1) ; doall(master)
End.

End.

ArchiveEntry "FM19/8 02 Solution: Speed Control Loop Invariant"
Description "Find a Loop Invariant for Braking".

Definitions       /* function symbols cannot change their value */
  Real D;         /* speed limit sign position */
  Real S;         /* posted speed limit */
  Real B;         /* brakes */
  Real ep;
  Real A;
End.

ProgramVariables  /* program variables may change their value over time */
  Real x, v, a;   /* car position, speed, and acceleration */
  Real t;         /* time */
End.

Problem
  x<=D & S>=0 & B>0 & v^2-S^2<=2*B*(D-x)
 ->
  [
    {
      { a := -B; }
      {x'=v, v'=a & v>=0}
    }*@invariant(v^2-S^2<=2*B*(D-x))
  ](x>=D -> v<=S)
End.

Tactic "Speed Control: Solution Automatic Proof"
  master
End.

End.

ArchiveEntry "FM19/8 03 Exercise: Speed Control Coasting Condition"
Description "Find a Control Condition for Coasting".

Definitions       /* function symbols cannot change their value */
  Real D;         /* speed limit sign position */
  Real S;         /* posted speed limit */
  Real B;         /* brakes */
  Real ep;        /* reaction time */
  Real A;
End.

ProgramVariables  /* program variables may change their value over time */
  Real x, v, a;   /* car position, speed, and acceleration */
  Real t;         /* time */
End.

Problem
  x<=S & S>=0 &B>0 & v^2-S^2<=2*B*(D-x) & ep>0
 ->
  [
    {
      {   a := -B;
       ++ ?v^2-S^2<=2*B*(D-x-__________); a:=0; }
      t:=0;
      {x'=v, v'=a, t'=1 & v>=0 & t<=ep}
    }*@invariant(v^2-S^2<=2*B*(D-x))
  ](x>=D -> v<=S)
End.

Tactic "Speed Control: Explore"
  explore
End.

End.

ArchiveEntry "FM19/8 04 Solution: Speed Control Coasting Condition"
Description "Find a Control Condition for Coasting".

Definitions       /* function symbols cannot change their value */
  Real D;         /* speed limit sign position */
  Real S;         /* posted speed limit */
  Real B;         /* brakes */
  Real ep;        /* reaction time */
  Real A;
End.

ProgramVariables  /* program variables may change their value over time */
  Real x, v, a;   /* car position, speed, and acceleration */
  Real t;         /* time */
End.

Problem
  x<=S & S>=0 &B>0 & v^2-S^2<=2*B*(D-x) & ep>0
 ->
  [
    {
      {   a := -B;
       ++ ?v^2-S^2<=2*B*(D-x-v*ep); a:=0; }
      t:=0;
      {x'=v, v'=a, t'=1 & v>=0 & t<=ep}
    }*@invariant(v^2-S^2<=2*B*(D-x))
  ](x>=D -> v<=S)
End.

Tactic "Speed Control: Solution Interactive Proof"
  implyR(1) ; loop("v^2-S^2<=2*B*(D-x)", 1) ; <(
    id,
    QE,
    composeb(1) ; composeb(1.1) ; solve(1.1.1) ;
    assignb(1.1) ; choiceb(1) ; andR(1) ; <(
      assignb(1) ; QE,
      composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; QE
    )
  )
End.

Tactic "Speed Control: Solution Automatic Proof"
  master
End.

End.

ArchiveEntry "FM19/8 05 Exercise: Accelerating Car"
Description "Find a Control Condition for Accelerating".

Definitions       /* function symbols cannot change their value */
  Real D;         /* speed limit sign position */
  Real S;         /* posted speed limit */
  Real B;         /* brakes */
  Real ep;        /* reaction time */
  Real A;         /* maximum acceleration */
End.

ProgramVariables  /* program variables may change their value over time */
  Real x, v, a;   /* car position, speed, and acceleration */
  Real t;         /* time */
End.

Problem
  x<=S & S>=0 &B>0 & v^2-S^2<=2*B*(D-x) & ep>0 & __________
 ->
  [
    {
      {   a := -B;
       ++ ?v^2-S^2<=2*B*(D-x-v*ep); a:=0;
       ++ ?__________;a:=A; }
      t:=0;
      {x'=v, v'=a, t'=1 & v>=0 & t<=ep}
    }*@invariant(v^2-S^2<=2*B*(D-x))
  ](x>=D -> v<=S)
End.

Tactic "Accelerating Car: Explore"
  explore
End.

End.

ArchiveEntry "FM19/8 06 Solution: Accelerating Car"
Description "Find a Control Condition for Coasting".

Definitions       /* function symbols cannot change their value */
  Real D;         /* speed limit sign position */
  Real S;         /* posted speed limit */
  Real B;         /* brakes */
  Real ep;        /* reaction time */
  Real A;         /* maximum acceleration */
End.

ProgramVariables  /* program variables may change their value over time */
  Real x, v, a;   /* car position, speed, and acceleration */
  Real t;         /* time */
End.

Problem
  x<=S & S>=0 &B>=0 & v^2-S^2<=2*B*(D-x) & ep>0 & A>=0
 ->
  [
    {
      {   a := -B;
       ++ ?v^2-S^2<=2*B*(D-x-v*ep); a:=0;
       ++ ?(v+A*ep)^2-S^2<=2*B*(D-x-v*ep-A/2*ep^2); a:=A; }
      t:=0;
      {x'=v, v'=a, t'=1 & v>=0 & t<=ep}
    }*@invariant(v^2-S^2<=2*B*(D-x))
  ](x>=D -> v<=S)
End.

Tactic "Speed Control: Explore"
  explore
End.

End.

ArchiveEntry "FM19/8 07 Car Drives Curve"

Description "Car picks steering to not exceed maximum angular speed".

Description "Find a Control Condition for Coasting".

Definitions       /* function symbols cannot change their value */
  Real ep;        /* reaction time */
  Real W;         /* maximum angular speed before tires slip */
  Real A;
  Real B;
End.

ProgramVariables   /* program variables may change their value over time */
  Real x, y, v, a; /* car position, speed, and acceleration */
  Real k, w;       /* steering, angular speed */
  Real t;          /* time */
End.

Problem
  B>0 & A>=0 & ep>0 & W>=0 & abs(w)<=W
 ->
  [
    {
      a:=*; ?(-B<=a & a<=A);
      k:=*; ?((a>=0&abs(k)*(v+a*ep)<=W) | (a<=0&abs(k)*v<=W));
      w:=v*k;
      t:=0;
      {{x'=-k*y*v, y'=k*x*v, v'=a, w'=a*k,
       t'=1 & v>=0 & t<=ep}@invariant(t>=0,w=v*k,v=old(v)+a*t)}
    }*@invariant(abs(w)<=W)
  ]abs(w)<=W
End.

Tactic "Proof"
implyR(1) ; loop("abs(w)<=W()", 1) ; <(
  id,
  id,
  unfold ; dC("t>=0&w=v*k", 1) ; <(
    dC("v=old(v)+a*t", 1) ; <(
      dW(1) ; QE,
      dI(1)
      ),
    dI(1)
    )
  )
End.

End.