ArchiveEntry "11: Aerodynamic Acrophobic Bouncing Ball". /** * 11: Aerodynamic Acrophobic Bouncing Ball */ ProgramVariables. /* program variables may change their value over time */ R x. /* height of ball */ R v. /* velocity of ball */ End. Functions. /* function symbols cannot change their value */ R H. /* initial height of ball */ R g. /* gravitational constant */ R c. /* elastic damping factor for bounce on the floor (x=0) */ R r. /* aerodynamic damping factor in the air / air resistance */ End. Problem. x<=H & v=0 & x>=0 & (g>0 & 1>=c&c>=0 & r>=0) -> [ { {?x=0; v:=-c*v; ++ ?x!=0;} {{x'=v,v'=-g-r*v^2&x>=0&v>=0} ++ {x'=v,v'=-g+r*v^2&x>=0&v<=0}} }*@invariant(2*g*x<=2*g*H-v^2&x>=0) ] (0<=x&x<=H) End. Tactic "11: Aerodynamic Acrophobic Bouncing Ball: generalizing as in book". implyR(1) ; loop({`2*g()*x<=2*g()*H()-v^2&x>=0`}, 1) ; <( QE, QE, composeb(1) ; MR({`2*g()*x<=2*g()*H()-v^2&x>=0&g()>0&r()>=0`}, 1) ; <( choiceb(1) ; andR(1) ; <( composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; QE, testb(1) ; implyR(1) ; QE ), choiceb(1) ; andR(1) ; <( dC({`2*g()*x<=2*g()*H()-v^2`}, 1) ; <( dW(1) ; QE, dI(1) ), dC({`2*g()*x<=2*g()*H()-v^2`}, 1) ; <( dW(1) ; QE, dI(1) ) ) ) ) End. Tactic "11: Aerodynamic Acrophobic Bouncing Ball: top-level". implyR(1) ; loop({`2*g()*x<=2*g()*H()-v^2&x>=0`}, 1) ; <( QE, QE, composeb(1) ; choiceb(1) ; composeb(1.0) ; testb(1.0) ; andR(1) ; <( implyR(1) ; assignb(1) ; choiceb(1) ; andR(1) ; <( dC({`2*g()*x<=2*g()*H()-v^2`}, 1) ; <( dW(1) ; QE, dI(1) ), dC({`2*g()*x<=2*g()*H()-v^2`}, 1) ; <( dW(1) ; QE, dI(1) ) ), testb(1) ; implyR(1) ; choiceb(1) ; andR(1) ; <( dC({`2*g()*x<=2*g()*H()-v^2`}, 1) ; <( dW(1) ; QE, dI(1) ), dC({`2*g()*x<=2*g()*H()-v^2`}, 1) ; <( dW(1) ; QE, dI(1) ) ) ) ) End. Tactic "11: Aerodynamic Acrophobic Bouncing Ball: automatic". master End. End. ArchiveEntry "11: Bouncing Ball". /** * 11: Quantum the Acrophobic Bouncing Ball * As in chapter 7 */ Functions. /* function symbols cannot change their value */ R H. /* initial height */ R g. /* gravity */ R c. /* damping coefficient */ End. ProgramVariables. /* program variables may change their value over time */ R x. /* height */ R v. /* velocity */ End. Problem. x>=0 & x=H & v=0 & g>0 & 1=c&c>=0 -> [ { {x'=v,v'=-g&x>=0} {?x=0; v:=-c*v; ++ ?x!=0;} }*@invariant(2*g*x=2*g*H-v^2 & x>=0) ] (x>=0 & x<=H) End. Tactic "11: Bouncing Ball: differential invariants". implyR(1) ; loop({`2*g()*x=2*g()*H()-v^2&x>=0`}, 1) ; <( QE, QE, composeb(1) ; MR({`2*g()*x=2*g()*H()-v^2&x>=0&g()>0&1=c()`}, 1) ; <( boxAnd(1) ; andR(1) ; <( dI(1), dW(1) ; prop ), choiceb(1) ; andR(1) ; <( composeb(1) ; testb(1) ; implyR(1) ; assignb(1) ; QE, testb(1) ; prop ) ) ) End. End. ArchiveEntry "11: Damped Oscillator". Functions. /* function symbols cannot change their value */ R w(). /* undamped angular frequency */ R c(). /* level of ellipse */ R d(). /* constant damping ratio */ End. ProgramVariables. /* program variables may change their value over time */ R x. /* position of spring/mass system */ R 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 "11: Damped Oscillator: Differential invariant proof". implyR(1) ; dI(1) End. End. ArchiveEntry "11: Increasingly Damped Oscillator". Functions. R w(). /* undamped angular frequency */ R c(). /* level of ellipse */ End. ProgramVariables. R x. /* position of spring/mass system */ R y. /* velocity */ R 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 "11: Increasingly Damped Oscillator: Differential cut proof". implyR(1) ; dC({`d>=0`}, 1) ; <( dI(1), dI(1) ) End. End.