/* Exported from KeYmaera X v5.0.1 */ Theorem "LFCPS Exercise/Ex 3.1 2D Avoid a Point" Definitions Real ox; /* x-coordinate of the obstacle */ Real oy; /* y-coordinate of the obstacle */ Bool safe(Real x, Real y, Real vx, Real vy) <-> (vx!=0&y+vy/vx*(ox-x)!=oy) | (vy!=0&x+vx/vy*(oy-y)!=ox); /* condition for controller to choose velocity (vx vy) */ End. ProgramVariables Real x; /* x-coordinate of the car */ Real y; /* y-coordinate of the car */ Real vx; /* (vx,vy) velocity of the car*/ Real vy; End. Problem (x!=ox|y!=oy) /* start not collided with obstacle */ -> [{ {vx:=*; vy:=*; ?safe(x,y, vx, vy);} /* Controller chooses velocity with the restriction that it satisfies the safety condition */ {x'=vx,y'=vy} /* linear motion with 0 acceleration */ }* @invariant(x != ox | y != oy) /* the loop invariant */ ]!(x=ox&y=oy) /* safe if no collision with obstacle */ End. End. /* Exported from KeYmaera X v5.0.1 */ Theorem "LFCPS Exercise/Ex 3.2 2D Avoid a Point (timed control)" Definitions Real ox; /* x-coordinate of obstacle */ Real oy; /* y-coordinate of obstacle */ Bool safe(Real x, Real y, Real vx, Real vy) <-> (x-ox)*(x+T*vx-ox)>0 | (y-oy)*(y+T*vy-oy)>0; /* velocity (vx,vy) is safe as long as following the continuous dynamics for any time <=T does not lead to a collision */ Real T; /* maximum time to elapse between control cycles */ End. ProgramVariables Real x; /* x-coordinate of car */ Real y; /* y-coordinate of car */ Real vx; /* (vx, vy)) velocity of car */ Real vy; Real t; /* timer variable */ End. Problem (x!=ox|y!=oy)-> /* start not collided with obstacle */ [{ {vx:=*; vy:=*; ?safe(x,y,vx,vy);} /* Controller chooses velocity with the restriction that it satisfies the safety condition */ t:=0; /* reset timer variable */ {x'=vx,y'=vy,t'=1&t<=T} /* linear motion with additional time variable and evolution domain constraint ensuring execution of controller within time interval [0,T] */ }* @invariant(x!=ox|y!=oy) ](x!=ox|y!=oy) /* safe if no collision with obstacle */ End. End. /* Exported from KeYmaera X v5.0.1 */ Theorem "LFCPS Exercise/Ex 3.3 An Event-Triggered Ping Pong Ball" Definitions Real g; /* gravity constant */ Real f; /* paddle damping factor */ Real c; /* ground damping factor */ End. ProgramVariables Real x; /* height of ping pong ball */ Real v; /* velocity of ping pong ball */ End. Problem (g>0 & f>0 & c>0 & 1>c & x=5 & v<=0) /* assumptions about constants and initial state */ -> [{ {{x'=v, v'=-g & x>=0 & x<=5} ++ {x'=v, v'=-g & x>=5}} /* dynamics of bouncing ball; overlapping evolution domain constraints ensure that controller is triggered when x=5 at the latest */ {?x=0;v:=-c*v;++?x!=0;} /* discrete model of the physics of hitting the ground */ {?(x>=4&x<=5&v>=0);v:=-f*v;++?(x<5);} /* if the ball is climbing, possibly hit it with the paddle if 4<=x<=5 and certainly hit if x=5 */ }* @invariant(0<=x&x<=5&(x=5->v<=0)) ] (0<=x & x<=5) /* acrophobic bouncing ball is safe */ End. /* Exported from KeYmaera X v5.0.1 */ Theorem "LFCPS Exercise/Ex 3.4 Time-Triggered Ping-Pong Ball" Definitions Real H; /* initial height */ Real g; /* gravity */ Real c; /* damping coefficient */ Real f; /* paddle factor */ End. ProgramVariables Real x, v; /* height, velocity */ Real t; /* time */ End. Problem (2*x=2*H-v^2 & 0<=x&x<=5 & v<=0) & (g=1&g>0 & 1=c&c>=0 & 1=f&f>=0) -> [ { {{?x=0; v:=-c*v; ++ ?x!=0;} {?((x>5+1/2-v | 2*x>2*5-v^2&v<1) & v>=0); v:=-f*v; ++ ? !((x>5+1/2-v | 2*x>2*5-v^2&v<1) & v>=0);}} t:=0; {x'=v,v'=-g,t'=1 & x>=0&t<=1} }* @invariant(2*x=2*H-v^2 & (x>=0&x<=5)) ] (0<=x&x<=5) End. End.