/* 2D Problems */ ArchiveEntry "Benchmarks/Nonlinear/Ahmadi Parrilo Krstic" Description "Theorem 1.1 (1)". Citation "Amir Ali Ahmadi, Miroslav Krstic, and Pablo A; Parrilo. A globally asymptotically stable polynomial vector field with no polynomial Lyapunov function; CDC-ECE 2011". Link "https://doi.org/10.1109/CDC.2011.6161499". ProgramVariables Real x; Real y; End. Problem 0.5<=x & x<=0.7 & 0<=y & y<=0.3 -> [ {x'=-x+x*y , y'=-y}@invariant(y>=0) ] !(-0.8>=x & x>=-1 & -0.7>=y & y>=-1) End. Tactic "Scripted proof" implyR(1); dC("y>=0",1); <( dW(1); QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Arrowsmith Place Fig_3_11 page 83" Description "Fig 3.11 Page 83". Citation "D. K. Arrowsmith and C. M. Place. An Introduction to Dynamical Systems". ProgramVariables Real x; Real y; End. Problem x=1 & y=1/8 -> [ {x'=x-y^2, y'=y*(x-y^2)}@invariant(y^2 < x) ] !(x<0) End. Tactic "Scripted proof" implyR(1); dC("y^2 < x",1); <( dW(1); QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Arrowsmith Place Fig_3_5e page 79" Description "Fig 3.5e Page 79". Citation "D. K. Arrowsmith and C. M. Place. An Introduction to Dynamical Systems". ProgramVariables Real x; Real y; End. Problem x=1 & y=-1 -> [ {x'=x^2+(x+y)/2, y'=(-x+3*y)/2}@invariant(y-x+1<=0 & y<=0) ] !(y>0) End. Tactic "Scripted proof" implyR(1); dC("y-x+1<=0 & y<=0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Ben Sassi Girard 20104 Moore-Greitzer Jet" Description "6.1 Moore-Greitzer jet engine model". Citation "Mohamed Amin Ben Sassi, Antoine Girard. Controller synthesis for robust invariance of polynomial dynamical systems using linear programming". Link "https://doi.org/10.1016/j.sysconle.2012.01.004". ProgramVariables Real x; Real y; End. Problem -1/5000 + (1/20+x)^2 + (3/200 + y)^2 <= 0 -> [ {x'=(-3*x^2)/2-x^3/2-y, y'=3*x-y}@invariant(0.073036*x^6-0.014461*x^5*y+0.059693*x^4*y^2-0.0063143*x^3*y^3+0.029392*x^2*y^4+0.0036316*y^6+0.064262*x^5+0.24065*x^4*y-0.082711*x^3*y^2+0.28107*x^2*y^3-0.015542*x*y^4+0.036437*y^5+0.47415*x^4-0.56542*x^3*y+1.1849*x^2*y^2-0.22203*x*y^3+0.19053*y^4-0.59897*x^3+1.8838*x^2*y-0.59653*x*y^2+0.47413*y^3+1.0534*x^2-0.51581*x*y+0.43393*y^2-0.35572*x-0.11888*y-0.25586<=0) ] !(49/100 + x + x^2 + y + y^2 <= 0) End. Tactic "Scripted proof" useSolver("Mathematica"); implyR(1); dC("0.073036*x^6-0.014461*x^5*y+0.059693*x^4*y^2-0.0063143*x^3*y^3+0.029392*x^2*y^4+0.0036316*y^6+0.064262*x^5+0.24065*x^4*y-0.082711*x^3*y^2+0.28107*x^2*y^3-0.015542*x*y^4+0.036437*y^5+0.47415*x^4-0.56542*x^3*y+1.1849*x^2*y^2-0.22203*x*y^3+0.19053*y^4-0.59897*x^3+1.8838*x^2*y-0.59653*x*y^2+0.47413*y^3+1.0534*x^2-0.51581*x*y+0.43393*y^2-0.35572*x-0.11888*y-0.25586<=0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" useSolver("Mathematica"); auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Ben Sassi Girard Sankaranarayanan 2014 Fitzhugh-Nagumo" Description "Fitzhugh-Nagumo system". Citation "Mohamed Amin Ben Sassi, Antoine Girard, Sriram Sankaranarayanan. Iterative computation of polyhedral invariants sets for polynomial dynamical systems". Link "10.1109/CDC.2014.7040384". ProgramVariables Real x; Real y; End. Problem -1/20 + (5/4+x)^2 + (-5/4+y)^2 <= 0 -> [ {x'=7/8+x-x^3/3-y, y'=(2*(7/10+x-(4*y)/5))/25}@invariant(x*((-73)+23*x) < 157+y*(134+81*y)) ] !(36/5 + 5*x + x^2 + 2*y + y^2 <= 0) End. Tactic "Scripted proof" implyR(1); dC("x*((-73)+23*x) < 157+y*(134+81*y)",1); <( dW(1); QE, barrier(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("0.12152*x^4+0.22807*x^3*y+0.214*x^2*y^2-0.71222*y^4-0.27942*x^3-0.48799*x^2*y-0.2517*x*y^2-0.3366*y^3-0.21526*x^2+0.16728*x*y-0.44613*y^2+0.35541*x-0.21594*y-0.72852<=0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Bhatia Szego Ex_2_4 page 68" Description "Ex 2.4 Page 68". Citation "Bhatia, N. P. and Szego, G. P.. Stability Theory of Dynamical Systems". ProgramVariables Real x; Real y; End. Problem x^2 + (-1/2 + y)^2 < 1/24 -> [ {x'=-x+2*x^3*y^2 , y'=-y & x^2*y^2<1}@invariant(4*x*(1821+5601250*x)+4827750*x*y+125*(76794+(-45619)*x^3)*y^2 < 1375*(4891+3332*y)) ] !(x <= -2 | y <= -1) End. Tactic "Scripted proof" useSolver("Mathematica"); implyR(1); dC("4*x*(1821+5601250*x)+4827750*x*y+125*(76794+(-45619)*x^3)*y^2 < 1375*(4891+3332*y)", 1); <( dW(1); QE, barrier(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("-0.00028346*x^6*y^3 - 0.00049999*x^5*y^4 + 0.00018784*x^4*y^5 + 0.0002836*x^3*y^6 - 0.00020211*x^2*y^7 - 0.00011251*x*y^8 + 0.00032872 *y^9 - 0.00032162*x^7*y - 0.0012954*x^6*y^2 - 0.0038775*x^5*y^3 - 0.0085289*x^4*y^4 + 0.0016293*x^3*y^5 + 0.0018949*x^2*y^6 - 0.0035577 *x*y^7 + 0.011859*y^8 - 0.00043993*x^7 - 0.0050214*x^6*y - 0.0047617*x^5 *y^2 + 0.011009*x^4*y^3 + 0.012178*x^3*y^4 + 0.0055785*x^2*y^5 + 0.0037099*x*y^6 - 0.062198*y^7 - 0.0023971*x^6 + 0.005244*x^5*y + 0.0031699*x^4*y^2 + 0.00069299*x^3*y^3 + 0.14159*x^2*y^4 - 0.081176*x *y^5 + 0.27277*y^6 + 0.0089006*x^5 + 0.10703*x^4*y + 0.0021026*x^3*y^2 - 0.39217*x^2*y^3 + 0.17202*x*y^4 - 0.85217*y^5 + 0.052331*x^4 - 0.008468*x^3*y - 0.21988*x^2*y^2 - 0.19426*x*y^3 + 1.3672*y^4 - 0.067608*x^3 - 1.3917*x^2*y - 1.3541*x*y^2 - 1.0593*y^3 - 0.80894*x^2 - 2.9459*x*y + 1.0078*y^2 - 1.8819*x - 2.2726*y - 1.433 <= 0 & y>=0 & x>=-2",1); <( dW(1); QE, ODEinv(1) /* todo */ ) End. Tactic "Automated proof (from annotations)" useSolver("Mathematica"); auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Collin Goriely page 60" ProgramVariables Real x; Real y; End. Problem (2+x)^2 + (-1+y)^2 <= 1/4 -> [ {x'=x^2+2*x*y+3*y^2, y'=2*y*(2*x+y)}@invariant(x0) End. Tactic "Scripted proof" implyR(1) ; dC("x < y", 1) ; <( dC("x+y < 0", 1) ; <( dW(1) ; QE, dbx(1) ), dbx(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("y>=0 & x+y<=0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dai Gan Xia Zhan JSC14 Ex. 2" Description "Example 2". Citation "Liyun Dai, Ting Gan, Bican Xia, Naijun Zhan. Barrier certificates revisited; J. Symb. Comput.". Link "https://doi.org/10.1016/j.jsc.2016.07.010". ProgramVariables Real x; Real y; End. Problem x^2 + (2+y)^2 <= 1 -> [ {x'=2*x-x*y, y'=2*x^2-y}@invariant(0.0052726*x^10+0.013182*x^8*y^2+0.013181*x^6*y^4+0.0065909*x^4*y^6+0.0016477*x^2*y^8+0.00016477*y^10-0.060426*x^8*y-0.11666*x^6*y^3-0.08401*x^4*y^5-0.02829*x^2*y^7-0.0026618*y^9-0.0093935*x^8+0.25715*x^6*y^2+0.35556*x^4*y^4+0.18385*x^2*y^6+0.017843*y^8-0.22922*x^6*y-0.82409*x^4*y^3-0.6654*x^2*y^5-0.072582*y^7+0.38533*x^6+1.6909*x^4*y^2+1.7759*x^2*y^4+0.20099*y^6+1.8855*x^4*y-0.83113*x^2*y^3-0.10854*y^5-4.9159*x^4-11.581*x^2*y^2-1.9047*y^4+6.644*x^2*y+7.8358*y^3+1.5029*x^2-13.2338*y^2+10.8962*y-3.4708<=0&0.10731*x^10+0.26827*x^8*y^2+0.26827*x^6*y^4+0.13413*x^4*y^6+0.033534*x^2*y^8+0.0033532*y^10-1.2677*x^8*y-2.4914*x^6*y^3-1.8208*x^4*y^5-0.59588*x^2*y^7-0.057773*y^9-0.82207*x^8+4.1107*x^6*y^2+6.7924*x^4*y^4+3.4828*x^2*y^6+0.36938*y^8+6.8306*x^6*y-0.93431*x^4*y^3-5.9328*x^2*y^5-0.95223*y^7+2.2556*x^6-17.4284*x^4*y^2-6.4448*x^2*y^4-0.33741*y^6-1.2936*x^4*y+16.8675*x^2*y^3+8.8828*y^5-16.1915*x^4-39.7751*x^2*y^2-25.8126*y^4+43.7284*x^2*y+39.2116*y^3-12.7866*x^2-33.0675*y^2+15.2878*y-3.1397<=0) ] !(x^2+(-1+y)^2 <= 9/100) End. Tactic "Scripted proof" useSolver("Mathematica"); implyR(1); dC("0.0052726*x^10+0.013182*x^8*y^2+0.013181*x^6*y^4+0.0065909*x^4*y^6+0.0016477*x^2*y^8+0.00016477*y^10-0.060426*x^8*y-0.11666*x^6*y^3-0.08401*x^4*y^5-0.02829*x^2*y^7-0.0026618*y^9-0.0093935*x^8+0.25715*x^6*y^2+0.35556*x^4*y^4+0.18385*x^2*y^6+0.017843*y^8-0.22922*x^6*y-0.82409*x^4*y^3-0.6654*x^2*y^5-0.072582*y^7+0.38533*x^6+1.6909*x^4*y^2+1.7759*x^2*y^4+0.20099*y^6+1.8855*x^4*y-0.83113*x^2*y^3-0.10854*y^5-4.9159*x^4-11.581*x^2*y^2-1.9047*y^4+6.644*x^2*y+7.8358*y^3+1.5029*x^2-13.2338*y^2+10.8962*y-3.4708<=0&0.10731*x^10+0.26827*x^8*y^2+0.26827*x^6*y^4+0.13413*x^4*y^6+0.033534*x^2*y^8+0.0033532*y^10-1.2677*x^8*y-2.4914*x^6*y^3-1.8208*x^4*y^5-0.59588*x^2*y^7-0.057773*y^9-0.82207*x^8+4.1107*x^6*y^2+6.7924*x^4*y^4+3.4828*x^2*y^6+0.36938*y^8+6.8306*x^6*y-0.93431*x^4*y^3-5.9328*x^2*y^5-0.95223*y^7+2.2556*x^6-17.4284*x^4*y^2-6.4448*x^2*y^4-0.33741*y^6-1.2936*x^4*y+16.8675*x^2*y^3+8.8828*y^5-16.1915*x^4-39.7751*x^2*y^2-25.8126*y^4+43.7284*x^2*y+39.2116*y^3-12.7866*x^2-33.0675*y^2+15.2878*y-3.1397<=0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" useSolver("Mathematica"); auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dai Gan Xia Zhan JSC14 Ex. 5" Description "Example 5". Citation "Liyun Dai, Ting Gan, Bican Xia, Naijun Zhan. Barrier certificates revisited; J. Symb. Comput.". Link "https://doi.org/10.1016/j.jsc.2016.07.010". ProgramVariables Real x; Real y; End. Problem (1+x)^2 + ((-2)+y)^2 <= 4/25 -> [ {x'=y, y'=2*x-x^3-y-x^2*y}@invariant(0.23942*x^6 + 0.097208*x^5*y + 0.06013*x^4*y^2 - 0.0076888*x^3*y^3 - 0.022097*x^2*y^4 + 0.067444*x*y^5 + 0.063249*y^6 - 0.11511*x^5 - 0.093461*x^4*y - 0.061763*x^3*y^2 + 0.065902*x^2*y^3 + 0.053766*x*y^4 - 0.1151*y^5 - 0.95442*x^4 + 0.38703*x^3*y + 0.46309*x^2*y^2 - 0.14691*x *y^3 + 0.11756*y^4 - 0.021196*x^3 - 0.40047*x^2*y - 0.28433*x*y^2 - 0.028468*y^3 - 0.020192*x^2 - 0.37629*x*y - 0.13713*y^2 + 1.9803*x - 1.4121*y - 0.51895<=0) ] !(((-1)+x)^2 + y^2 <= 1/25) End. Tactic "Scripted proof" useSolver("Mathematica"); implyR(1); dC("0.23942*x^6 + 0.097208*x^5*y + 0.06013*x^4*y^2 - 0.0076888*x^3*y^3 - 0.022097*x^2*y^4 + 0.067444*x*y^5 + 0.063249*y^6 - 0.11511*x^5 - 0.093461*x^4*y - 0.061763*x^3*y^2 + 0.065902*x^2*y^3 + 0.053766*x*y^4 - 0.1151*y^5 - 0.95442*x^4 + 0.38703*x^3*y + 0.46309*x^2*y^2 - 0.14691*x*y^3 + 0.11756*y^4 - 0.021196*x^3 - 0.40047*x^2*y - 0.28433*x*y^2 - 0.028468*y^3 - 0.020192*x^2 - 0.37629*x*y - 0.13713*y^2 + 1.9803*x - 1.4121*y - 0.51895<=0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" useSolver("Mathematica"); auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Darboux Christoffel Int Goriely page 58" ProgramVariables Real x; Real y; End. Problem x^2+y^2<=1 -> [ {x'=3*((-4)+x^2), y'=3+x*y-y^2} @invariant( x^2<4, -0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0&(-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0, x^2+y^2-16<=0) ] !(x < (-4) | y < (-4) | x>4 | y>4) End. Tactic "Scripted proof" useSolver("Mathematica"); implyR('R=="x^2+y^2<=1->[{x'=3*((-4)+x^2),y'=3+x*y-y^2}](!(x < (-4)|y < (-4)|x>4|y>4))"); dC("-0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0&(-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0", 'R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2}](!(x < (-4)|y < (-4)|x>4|y>4))"); <( "Use": dC("x^2+y^2-16<=0", 'R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2&true&-0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0&(-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0}](!(x < (-4)|y < (-4)|x>4|y>4))"); <( "Use": dW('R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2&(true&-0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0&(-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0)&x^2+y^2-16<=0}](!(x < (-4)|y < (-4)|x>4|y>4))"); QE, "Show": ODEinv('R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2&true&-0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0&(-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0}]x^2+y^2-16<=0") ), "Show": boxAnd('R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2}](-0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0&(-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0)"); andR('R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2}]-0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0&[{x'=3*((-4)+x^2),y'=3+x*y-y^2}](-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0"); <( "[{x'=3*((-4)+x^2),y'=3+x*y-y^2}]-0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0": ODEinv('R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2}]-0.0013138*x^5+0.00048141*x^4*y+0.000828*x^2*y^3-0.0016748*x*y^4+0.0008106*y^5+0.010722*x^4-0.0018729*x^3*y+0.0041383*x^2*y^2-0.013911*x*y^3+0.0085091*y^4-0.039948*x^3-0.0060006*x^2*y-0.046355*x*y^2+0.054433*y^3-0.028132*x^2+0.13217*x*y+0.10916*y^2+0.62004*x-0.88775*y-1.1161<=0"), "[{x'=3*((-4)+x^2),y'=3+x*y-y^2}](-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0": dC("x^2<4", 'R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2}](-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0"); <( "Use": ODEinv('R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2&true&x^2 < 4}](-0.00011438)*x^4*y^2+0.00015105*x^2*y^4-0.0018063*x^5+0.0012699*x^3*y^2+0.0014498*x^2*y^3-0.0014334*x*y^4+0.0013001*y^5+0.017567*x^4+0.0050023*x^3*y-0.0016674*x^2*y^2-0.015315*x*y^3+0.01038*y^4-0.072259*x^3-0.035874*x^2*y-0.050558*x*y^2+0.058708*y^3-0.05097*x^2+0.042626*x*y+0.19257*y^2+1.3148*x+0.014613*y-1.2585<=0") , "Show": ODEinv('R=="[{x'=3*((-4)+x^2),y'=3+x*y-y^2}]x^2<4") ) ) ) End. Tactic "Automated proof (from annotations)" useSolver("Mathematica"); auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Djaballah Chapoutot Kieffer Bouissou 2017 Ex. 2" Description "Example 2, p. 293". Citation "Adel Djaballah, Alexandre Chapoutot, Michel Kieffer, Olivier Bouissou; Construction of parametric barrier functions for dynamical systems using interval analysis; Automatica 78 (2017) 287–296.". Link "https://doi.org/10.1016/j.automatica.2016.12.013". ProgramVariables Real x; Real y; End. Problem -1/20 + (5/4 + x)^2 + (-5/4 + y)^2 <= 0 -> [ {x'=x+y , y'=x*y-y^2/2}@invariant(y>0, y*((-104420)+(-73565)*x+18407*y) < 44444) ] !((5/2 + x)^2 + (-4/5 + y)^2 <= 1/20) End. Tactic "Scripted proof" implyR(1) ; dC("y>0", 1) ; <( dC("y*((-104420)+(-73565)*x+18407*y) < 44444", 1) ; <( dW(1) ; QE, barrier(1) ), dbx(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 10_11" Description "Exercise 10.11". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem x^2 + y^2 < 1/4 -> [ {x'=(-70)-100*x+70*x^2+100*x^3-200*y+200*x^2*y, y'=146*x+100*y+140*x*y+100*x^2*y+200*x*y^2} @invariant(1+x>0, x < 1) ] !(2*x >= 3 | x <= (-3)/2) End. Tactic "Scripted proof" implyR('R=="x^2+y^2 < 1/4->[{x'=(-70)-100*x+70*x^2+100*x^3-200*y+200*x^2*y,y'=146*x+100*y+140*x*y+100*x^2*y+200*x*y^2}](!(2*x>=3|x<=(-3)/2))"); dC("1+x>0", 'R=="[{x'=(-70)-100*x+70*x^2+100*x^3-200*y+200*x^2*y,y'=146*x+100*y+140*x*y+100*x^2*y+200*x*y^2}](!(2*x>=3|x<=(-3)/2))"); <( "Use": dC("x < 1", 'R=="[{x'=(-70)-100*x+70*x^2+100*x^3-200*y+200*x^2*y,y'=146*x+100*y+140*x*y+100*x^2*y+200*x*y^2&true&1+x>0}](!(2*x>=3|x<=(-3)/2))"); <( "Use": dW('R=="[{x'=(-70)-100*x+70*x^2+100*x^3-200*y+200*x^2*y,y'=146*x+100*y+140*x*y+100*x^2*y+200*x*y^2&(true&1+x>0)&x < 1}](!(2*x>=3|x<=(-3)/2))"); QE, "Show": ODEinv('R=="[{x'=(-70)-100*x+70*x^2+100*x^3-200*y+200*x^2*y,y'=146*x+100*y+140*x*y+100*x^2*y+200*x*y^2&true&1+x>0}]x < 1") ), "Show": ODEinv('R=="[{x'=(-70)-100*x+70*x^2+100*x^3-200*y+200*x^2*y,y'=146*x+100*y+140*x*y+100*x^2*y+200*x*y^2}]1+x>0") ) End. Tactic "Automated proof" autoClose End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 10_11b" Description "Exercise 10.11b". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem (-1 + x)^2 + (1 + y)^2 < 1/4 -> [ {x'=1+x+x^2+x^3+2*y+2*x^2*y, y'=-y+2*x*y+x^2*y+2*x*y^2}@invariant(y<0) ] !(y >= 1) End. Tactic "Scripted proof" implyR(1) ; dC("y < 0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 10_15_i" Description "Exercise 10.15". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem x > -1 & x < -3/4 & y <= 3/2 & y >= 1 -> [ {x'=-42*x^7+50*x^2*y+156*x^3*y+258*x^4*y-46*x^5*y+68*x^6*y+20*x*y^6-8*y^7, y'=y*(1110*x^6-3182*x^4*y-220*x^5*y+478*x^3*y^3+487*x^2*y^4-102*x*y^5-12*y^6)}@invariant(y>0) ] !(x > 1 + y) End. Tactic "Scripted proof" implyR(1) ; dC("y>0", 1) ; <( dbx(1), dbx(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 10_15_ii" Description "Exercise 10.15 (modified)". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem x > -1 & x < -1/2 & y <= -1/10 & y >= -3/10 -> [ {x'=315*x^7+477*x^6*y-113*x^5*y^2+301*x^4*y^3-300*x^3*y^4-192*x^2*y^5+128*x*y^6-16*y^7, y'=y*(2619*x^6-99*x^5*y-3249*x^4*y^2+1085*x^3*y^3+596*x^2*y^4-416*x*y^5+64*y^6)}@invariant(x 1 + y) End. Tactic "Scripted proof" implyR(1) ; dC("x < y", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 10_9" Description "Exercise 10.9". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem (-1 + x)^2 + (1 + y)^2 < 1/4 -> [ {x'=x^4+2*x*y^2-6*x^2*y^2+y^4+x*(x^2-y^2), y'=2*x^2*y-4*x^3*y+4*x*y^3-y*(x^2-y^2)}@invariant(y < 0) ] !(y>=1) End. Tactic "Scripted proof" implyR(1) ; dC("y < 0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 1_11a" Description "Exercise 1.11". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem x > -1/2 & x < -1/3 & y < 0 & y >= -1/2 -> [ {x'=2*x-x^5-x*y^4, y'=y-x^2*y-y^3}@invariant(x < 0, y < 0) ] !(x + y > 0) End. Tactic "Scripted proof" implyR(1) ; dC("x < 0", 1) ; <( dC("y < 0", 1) ; <( dW(1) ; QE, dbx(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 1_9a" Description "Example 1.9a". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem x>-1/2 & x < -1/3 & y<0 & y>=-1/2 -> [ {x'=x*(1-x^2-y^2)+y*((-1+x^2)^2+y^2), y'=y*(1-x^2-y^2)-y*((-1+x^2)^2+y^2)}@invariant(y < 0, x+y < 0) ] !(x>=0) End. Tactic "Scripted proof" implyR(1) ; dC("y < 0", 1) ; <( dC("x+y < 0", 1) ; <( dbx(1), dbx(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 5_2" Description "Example 5.2". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem x > (-1) & x < (-1)/2 & y < (-1)/2 & y >= (-1) -> [ {x'=y, y'=x^5-x*y}@invariant(x^5-x*y-4*x^3*y<=0, y<=0) ] !(x + y > 1) End. Tactic "Scripted proof" implyR(1) ; dC("x^5-x*y-4*x^3*y<=0", 1) ; <( dC("y<=0", 1) ; <( dW(1) ; QE, ODEinv(1) ), ODEinv(1) ) End. Tactic "Scripted proof (2) fails" implyR(1); dC("x+1/2<=0 & y+1/2<=0",1); <( dW(1); QE, ODEinv(1) /* todo */ ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Dumortier Llibre Artes Ex. 5_2_ii" Description "Exercise 5.2 ii". Citation "Freddy Dumortier, Jaume Llibre, Joan C. Artes. Qualitative Theory of Planar Differential Systems". ProgramVariables Real x; Real y; End. Problem x > -4/5 & x < -1/3 & y < 0 & y >= -1 -> [ {x'=2*x-2*x*y, y'=-x^2+2*y+y^2}@invariant(x < 0, y < 0) ] !((x = 0 & y = 0) | x + y > 1) End. Tactic "Scripted proof" implyR(1); dC("x < 0", 1); <( "Use": dC("y < 0", 1); <( "Use": dW(1); QE, "Show": dbx(1) ), "Show": dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Fitzhugh Nagumo Ben Sassi Girard 2" Description "Fitzhugh-Nagumo system (modified)". Citation "Mohamed Amin Ben Sassi, Antoine Girard, Sriram Sankaranarayanan. Iterative computation of polyhedral invariants sets for polynomial dynamical systems". Link "10.1109/CDC.2014.7040384". ProgramVariables Real a; Real y; End. Problem -1<=a & a<=-0.5 & 1<=y & y<=1.5 -> [ {a'=7/8+a-a^3/3-y, y'=(2*(7/10+a-(4*y)/5))/25}@invariant(0.12152*a^4+0.22807*a^3*y+0.214*a^2*y^2-0.71222*y^4-0.27942*a^3-0.48799*a^2*y-0.2517*a*y^2-0.3366*y^3-0.21526*a^2+0.16728*a*y-0.44613*y^2+0.35541*a-0.21594*y-0.72852<=0) ] !(-2.5<=a & a<=-2 & -2<=y & y<=-1.5) End. Tactic "Scripted proof" useSolver("Mathematica"); implyR(1); dC("0.12152*a^4+0.22807*a^3*y+0.214*a^2*y^2-0.71222*y^4-0.27942*a^3-0.48799*a^2*y-0.2517*a*y^2-0.3366*y^3-0.21526*a^2+0.16728*a*y-0.44613*y^2+0.35541*a-0.21594*y-0.72852<=0",1); <( dW(1); QE, barrier(1) ) End. Tactic "Automated proof (from annotations)" useSolver("Mathematica"); auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Forsman Phd Ex 6_1 page 99" ProgramVariables Real x; Real y; End. Problem x^2 + (-2 + y)^2 < 1/24 -> [ {x'=-x+2*x^2*y, y'=-y}@invariant(y>0, 12299+9595*x>0) ] !(x <= -2 | y <= -1) End. Tactic "Scripted proof" implyR(1) ; dC("y>0", 1) ; <( dC("12299+9595*x>0", 1) ; <( dW(1) ; QE, barrier(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Forsman Phd Ex 6_14 page 119" ProgramVariables Real x; Real y; End. Problem x^2 + (-1 + y)^2 < 1/8 -> [ {x'=-2*x+y^4, y'=-y+3*x*y^3}@invariant(y>0) ] !(y <= -1) End. Tactic "Scripted proof" implyR(1) ; dC("y>0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Hamiltonian System 1" ProgramVariables Real x; Real y; End. Problem (2/3 + x)^2 + y^2 <= 1/24 -> [ {x'=-2*y, y'=-2*x-3*x^2}@invariant(x^2*(1+x)<=1855/12521+y^2, x^2*(1+x)>=121/1235+y^2) ] !(x>0) End. Tactic "Scripted proof" implyR(1) ; dC("x^2*(1+x)<=1855/12521+y^2", 1) ; <( dC("x^2*(1+x)>=121/1235+y^2", 1) ; <( ODEinv(1), dI(1) ), dI(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("-(x^2+x^3-y^2)<0 & x<0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Hybrid Controller Mode 1" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". ProgramVariables Real x; Real y; End. Problem (x-9)^2+(y-20)^20 <= 4 -> [ {x'=y^2+10*y+25, y'=2*x*y+10*x-40*y-200 & 5<=x&x<=35}@invariant(5133+8*((-40)+x)*x>=4*y*(10+y)) ] y<=48 End. Tactic "Scripted proof" implyR(1) ; dC("5133+8*((-40)+x)*x>=4*y*(10+y)", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; cut("\exists u11 \exists u12 (u11^2+u12^2!=0 & invcluster(x,y,u11,u12)=0)") ; <( existsL('Llast)*2 ; dC("invcluster(x,y,u11,u12)=0", 1) ; <( dWplus(1); QE, ODEinv(1) ) , hideR(1) ; QE ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Hybrid Controller Mode 2" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". ProgramVariables Real x; Real y; End. Problem (x-9)^2+(y-20)^20 <= 4 -> [ {x'=-y^2-10*y-25, y'=8*x*y+40*x-160*y-800 & 5<=x&x<=35}@invariant(1961/13+x^2+1/8*y*(10+y)<=40*x) ] y<=48 End. Tactic "Scripted proof" implyR(1) ; dC("1961/13+x^2+1/8*y*(10+y)<=40*x", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; cut("\exists u21 \exists u22 (u21^2+u22^2!=0 & invcluster(x,y,u21,u22)=0)") ; <( existsL('Llast)*2 ; dC("invcluster(x,y,u21,u22)=0", 1) ; <( dWplus(1); QE, dI(1) ) , hideR(1) ; QE ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Invariant Clusters Example 6" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". ProgramVariables Real x; Real y; End. Problem (x+15)^2+(y-17)^2-1<=0 -> [ {x'=y^2, y'=x*y}@invariant(4490/41+x^2>=y^2) ] !((x-11)^2+(y-16.5)^2-1<=0) End. Tactic "Scripted proof" implyR(1) ; dC("4490/41+x^2>=y^2", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (2)" implyR(1); cut("\exists u1 \exists u3 (u1^2+u3^2!=0 & invcluster(x,y,u1,u3)=0)"); <( existsL('Llast)*2; dC("invcluster(x,y,u1,u3)=0", 1); doall(ODEinv(1)); done , hideR(1) ; QE ) End. Tactic "Scripted proof (3)" implyR(1); dC("x^2-y^2 - (old(x)^2-old(y)^2) = 0", 1); doall(ODEinv(1)); done End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Invariant Clusters Example 7" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". ProgramVariables Real x; Real y; End. Problem 1-(x+6)^2 - (y+6)^2 >= 0 -> [ {x'=y^2-2*y, y'=x^2+2*x}@invariant(3*x^2*(3+x)<=1181+3*((-3)+y)*y^2) ] !(1-(x-8.2)^2 - (y-4)^2 >= 0) End. Tactic "Scripted proof" implyR(1) ; dC("3*x^2*(3+x)<=1181+3*((-3)+y)*y^2", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (1)" implyR(1) ; cut("\exists u1 \exists u3 (u1^2+u3^2!=0 & invcluster(x,y,u1,u3)=0)") ; <( existsL('Llast)*2 ; dC("invcluster(x,y,u1,u3)=0", 1) ; <( dWplus(1) ; QE, dI(1) ) , hideR(1) ; QE ) End. Tactic "Scripted proof (2)" /* disprovable */ /*invcluster(x,y,-3081.9,7.1798)=0*/ implyR(1); dC("invcluster(x,y,-3081.9,21.539)<=0", 1); doall(ODEinv(1)); done End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Locally stable nonlinear system" ProgramVariables Real x; /* x-coordinate */ Real y; /* y-coordinate */ End. Problem x^2 <= 1/2 & (y + 2)^2 <= 1/3 -> [ {x'=-x + y - x^3, y'=-x - y + y^2}@invariant(2*x^2+(y+3/2)^2-4<=0) ] ((-1 + x)^2 + (-3/2 + y)^2 > 1/4) End. Tactic "Scripted proof" implyR(1) ; dC("2*x^2+(y+3/2)^2-4<=0", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/MIT astronautics Lyapunov" ProgramVariables Real x; /* x-coordinate */ Real y; /* y-coordinate */ End. Problem x^2 <= 1/2 & y^2 <= 1/3 -> [ {x'=y - x^7*(x^4 + 2*y^2 - 10), y'=-x^3 - 3*(y^5)*(x^4 + 2*y^2 - 10)} @invariant(x^4 + 2*y^2 <= 10) ] ((-2 + x)^2 + (-3 + y)^2 > 1/4) End. Tactic "Scripted proof" implyR('R=="x^2<=1/2&y^2<=1/3->[{x'=y-x^7*(x^4+2*y^2-10),y'=-x^3-3*y^5*(x^4+2*y^2-10)}](-2+x)^2+(-3+y)^2>1/4"); dC("x^4+2*y^2<=10", 'R=="[{x'=y-x^7*(x^4+2*y^2-10),y'=-x^3-3*y^5*(x^4+2*y^2-10)}](-2+x)^2+(-3+y)^2>1/4"); <( "Use": dW('R=="[{x'=y-x^7*(x^4+2*y^2-10),y'=-x^3-3*y^5*(x^4+2*y^2-10)&true&x^4+2*y^2<=10}](-2+x)^2+(-3+y)^2>1/4"); QE, "Show": dbx('R=="[{x'=y-x^7*(x^4+2*y^2-10),y'=-x^3-3*y^5*(x^4+2*y^2-10)}]x^4+2*y^2<=10") ) End. Tactic "Automated proof" autoClose End. End. ArchiveEntry "Benchmarks/Nonlinear/Man Maccallum Goriely Page 57" ProgramVariables Real x; Real y; End. Problem x^2 + y^2 <= 1/4 -> [ {x'=-y+2*x^2*y, y'=y+2*x*y^2}@invariant(2*x^2 < 1) ] !(x > 3) End. Tactic "Scripted proof" implyR(1) ; dC("2*x^2 < 1", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Nonlinear Circuit Example 3" Citation "Mohamed H. Zaki, William Denman, Sofiène Tahar, Guy Bois. Integrating Abstraction Techniques for Formal Verification of Analog Designs". ProgramVariables Real x1; Real x2; End. Problem x1>=2 & x2^2<=1 -> [ { x1'=-x2^3, x2'=x1-x1^3 }@invariant(x1^4>=50000/7143+2*x1^2+x2^4) ] x1>=1 End. Tactic "Scripted proof" implyR(1) ; dC("x1^4>=50000/7143+2*x1^2+x2^4", 1) ; <( barrier(1), dI(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Nonlinear Circuit Example 4" Citation "Mohamed H. Zaki, William Denman, Sofiène Tahar, Guy Bois. Integrating Abstraction Techniques for Formal Verification of Analog Designs". ProgramVariables Real x1; Real x2; End. Problem -1.1<=x1&x1<=-0.7 & 0.5<=x2&x2<=0.9 -> [ { x1'=-x2^3, x2'=x1-x1^3 } ] x1^2+x2-3<0 End. End. ArchiveEntry "Benchmarks/Nonlinear/Nonlinear Circuit RLC Circuit Oscillator" Citation "Mohamed H. Zaki, William Denman, Sofiène Tahar, Guy Bois. Integrating Abstraction Techniques for Formal Verification of Analog Designs". ProgramVariables Real Il; Real Vc; End. Problem Il=1 & Vc=1 -> [ { Il'=-Vc-1/5*Vc^2, Vc'=-2*Il-Il^2+Il^3 }@invariant(4993/2416+Il^4+2*Vc^2+4/15*Vc^3<=4/3*Il^2*(3+Il)) ] Vc<=3 End. Tactic "Scripted proof" implyR(1) ; dC("4993/2416+Il^4+2*Vc^2+4/15*Vc^3<=4/3*Il^2*(3+Il)", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("1-5*Il^3-15*Il^2+Vc^3+15/2*Vc^2+15/4*Il^4 <= 0", 1); /* invariant from paper */ <(ODEinv(1), ODEinv(1)) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Prajna PhD Thesis 2-4-1 Page 31 (Variant)" Description "Variant of Page 31 with x'=x instead of x'=y". Citation "Prajna, Stephen (2005) Optimization-based methods for nonlinear and hybrid systems verification; Dissertation (Ph.D.), California Institute of Technology.". Link "http://resolver.caltech.edu/CaltechETD:etd-05272005-144358". ProgramVariables Real x; Real y; End. Problem (-3/2 + x)^2 + y^2 <= 1/4 -> [ {x'=x, y'=-x+x^3/3-y}@invariant(x>0) ] !((1 + x)^2 + (1 + y)^2 <= 4/25) End. Tactic "Scripted proof" implyR(1) ; dC("x>0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Stable Limit Cycle 2" ProgramVariables Real a; Real y; End. Problem a^2 + y^2 < 1/16 -> [ {a'=a-a^3+y-a*y^2, y'=-a+y-a^2*y-y^3}@invariant(a^2+y^2<=1) ] !(a < -1 | y < -1 | a > 1 | y > 1) End. Tactic "Scripted proof" implyR(1) ; dC("a^2+y^2<=1", 1) ; <( dW(1) ; QE, ODEinv(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Strogatz Example 6_3_2" Description "Example 6.3.2". Citation "Steven H. Strogatz. nonlinear Dynamics And Chaos: With Applications To Physics, Biology, Chemistry, And Engineering". ProgramVariables Real x; Real y; End. Problem x > -4/5 & x < -1/3 & y < 3/2 & y >= 1 -> [ {x'=-x+x*(x^2+y^2), y'=x+y*(x^2+y^2)}@invariant(3305*(x+y)>596) ] !(x < -1/3 & y >= 0 & 2*y < 1 & x > -4/5) End. Tactic "Scripted proof" implyR(1) ; dC("3305*(x+y)>596", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Strogatz Example 6_8_3" Description "Example 6.8.3". Citation "Steven H. Strogatz. nonlinear Dynamics And Chaos: With Applications To Physics, Biology, Chemistry, And Engineering". ProgramVariables Real x; Real y; End. Problem 2*(-1/3 + x)^2 + y^2 < 1/16 -> [ {x'=x^2*y, y'=x^2-y^2}@invariant(x>0) ] !(x <= -2) End. Tactic "Scripted proof" implyR(1) ; dC("x>0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Strogatz Exercise 6_1_5" Description "Exercise 6.1.5". Citation "Steven H. Strogatz. nonlinear Dynamics And Chaos: With Applications To Physics, Biology, Chemistry, And Engineering". ProgramVariables Real x; Real y; End. Problem (-1/3 + x)^2 + 2*(-1/3 + y)^2 < 1/25 -> [ {x'=x*(2-x-y), y'=x-y}@invariant(x>0, 19801*x^2+10*y*((-22888)+11079*y)+x*(64611+33500*y) < 97121) ] !(x >= 2 | x <= -2) End. Tactic "Scripted proof" implyR(1) ; dC("x>0", 1) ; <( dC("19801*x^2+10*y*((-22888)+11079*y)+x*(64611+33500*y) < 97121", 1) ; <( dW(1) ; QE, barrier(1) ), dbx(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("x>=0 & y > 0 & x<2",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Strogatz Exercise 6_1_9 Dipole" Description "Exercise 6.1.9". Citation "Steven H. Strogatz. nonlinear Dynamics And Chaos: With Applications To Physics, Biology, Chemistry, And Engineering". ProgramVariables Real x; Real y; End. Problem (-1/3 + x)^2 + y^2 < 1/25 -> [ {x'=2*x*y, y'=-x^2+y^2}@invariant(x>0) ] !(x <= -2) End. Tactic "Scripted proof" implyR(1) ; dC("x>0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Strogatz Exercise 6_6_1 Reversible System" Description "Exercise 6.6.1". Citation "Steven H. Strogatz. nonlinear Dynamics And Chaos: With Applications To Physics, Biology, Chemistry, And Engineering". ProgramVariables Real x; Real y; End. Problem (-1/3 + x)^2 + (-1/3 + y)^2 < 1/16 -> [ {x'=(1-x^2)*y, y'=1-y^2}@invariant(1+x>0, x<1) ] !(x >= 2 | x <= -2) End. Tactic "Scripted proof" implyR(1) ; dC("1+x>0", 1) ; <( dC("x < 1", 1) ; <( dW(1) ; QE, dbx(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Strogatz Exercise 6_6_2 Limit Cycle" Description "Exercise 6.6.2". Citation "Steven H. Strogatz. nonlinear Dynamics And Chaos: With Applications To Physics, Biology, Chemistry, And Engineering". ProgramVariables Real x; Real y; End. Problem (-1/3 + x)^2 + (-1/3 + y)^2 < 1/16 -> [ {x'=y, y'=-x+y*(1-x^2-y^2)}@invariant(x^2+y^2 < 1, 346400*(x^2+y^2)>8503) ] !(x^2 + y^2 = 0 | x >= 2 | x <= -2) End. Tactic "Scripted proof" implyR(1) ; dC("x^2+y^2 < 1", 1) ; <( dC("346400*(x^2+y^2)>8503", 1) ; <( dW(1) ; QE, dbx(1) ), dbx(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("x^2 + y^2 - 2 <=0 & -(x^2 + y^2 - 0.01) <= 0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Strogatz Exercise 7_3_5" Description "Exercise 7.3.5". Citation "Steven H. Strogatz. nonlinear Dynamics And Chaos: With Applications To Physics, Biology, Chemistry, And Engineering". ProgramVariables Real x; Real y; End. Problem (-1/3 + x)^2 + (-1/3 + y)^2 < 1/16 -> [ {x'=-x-y+x*(x^2+2*y^2), y'=x-y+y*(x^2+2*y^2)}@invariant(x^2+y^2>0, 5*x^2+2*x*y+7*y^2 < 4) ] !((x = 0 & y = 0) | x <= -2 | y <= -1) End. Tactic "Scripted proof" implyR(1) ; dC("x^2+y^2>0", 1) ; <( dC("5*x^2+2*x*y+7*y^2 < 4", 1) ; <( dW(1) ; QE, dbx(1) ), dbx(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("-4/5 + x^2 + 2*x*y/5 + 7*y^2/5 <= 0 & x^2+y^2!=0",1); <( dW(1); QE, ODEinv(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Unstable Unit Circle 2" ProgramVariables Real b; Real y; End. Problem b = 1/2 & y = 1/2 -> [ {b'=-b+b^3-y+b*y^2, y'=b-y+b^2*y+y^3}@invariant(b^2+y^2 < 1) ] !(b^2 + y^2 > 2) End. Tactic "Scripted proof" implyR(1) ; dC("b^2+y^2 < 1", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Wien bridge oscillator" ProgramVariables Real x; /* x-coordinate */ Real y; /* y-coordinate */ End. Problem x^2 <= 1/2 & y^2 <= 1/3 -> [ {x'=-x - (1117*y)/500 + (439*y^3)/200 - (333*y^5)/500, y'=x + (617*y)/500 - (439*y^3)/200 + (333*y^5)/500} @invariant(x^2 + x*y + y^2 - 111/59 <= 0) ] (x - 4*y < 8) End. Tactic "Scripted proof" implyR(1) ; dC("x^2+x*y+y^2-111/59<=0", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Scripted proof (2)" implyR(1); dC("x^2 + x*y + y^2 - 111/59 <= 0", 1); doall(ODEinv(1)); done End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Wiggins Example 17_1_2" ProgramVariables Real x; Real y; End. Problem (-1/3 + x)^2 + (-1/3 + y)^2 < 1/16 -> [ {x'=(2+x)*(-((1-x)*x)+y), y'=-y}@invariant(2+x>0) ] !(x <= -5/2) End. Tactic "Scripted proof" implyR(1) ; dC("2+x>0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Wiggins Example 18_7_3_n" ProgramVariables Real x; Real y; End. Problem (-1/3 + x)^2 + (-1/3 + y)^2 < 1/16 -> [ {x'=-x+2*y+x^2*y+x^4*y^5, y'=-y-x^4*y^6+x^8*y^9}@invariant(y>0) ] !(x <= -1 | y <= -1) End. Tactic "Scripted proof" implyR(1) ; dC("y>0", 1) ; <( ODEinv(1), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C1" Description "Example C1 (initial set expanded)". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; End. Problem 4 <= x1 & x1 <= 4.5 & 1 <= x2 & x2 <= 2 -> [ {x1'=-11/2*x2 + x2^2 , x2' = 6*x1-x1^2 & 1 <= x1 & x1 <= 5 & 1 <= x2 & x2 <= 5}@invariant(349+4*((-9)+x1)*x1^2+x2^2*((-33)+4*x2)<=0) ] !( 1 <= x1 & x1 <= 2 & 2 <= x2 & x2 <= 3 ) End. Tactic "Scripted proof" implyR(1) ; dC("349+4*((-9)+x1)*x1^2+x2^2*((-33)+4*x2)<=0", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C3" Description "Example C3". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; End. Problem -1/5 <= x1 & x1 <= 1/5 & 3/10 <= x2 & x2 <= 7/10 -> [ {x1' = -x1 + 2*x1^3*x2^2, x2' = -x2 & -2 <= x1 & x1 <= 2 & -2 <= x2 & x2 <= 2}@invariant(x1*x2 < 1) ] !( -2 <= x1 & x1 <= -1 & -2 <= x2 & x2 <= -1 ) End. Tactic "Scripted proof" implyR(1) ; dC("x1*x2 < 1", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C4" Description "Example C4". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; End. Problem -1 <= x1 & x1 <= 0 & -1 <= x2 & x2 <= 0 -> [ {x1' = -1 + x1^2 + x2^2, x2' = 5*(-1 + x1*x2) & -2 <= x1 & x1 <= 2 & -2 <= x2 & x2 <= 2}@invariant(22667*x1^2+x2*(257910+6221*x2)+x1*(141840+15973*x2) < 42786) ] !( 1 <= x1 & x1 <= 2 & 1 <= x2 & x2 <= 2 ) End. Tactic "Scripted proof" implyR(1) ; dC("22667*x1^2+x2*(257910+6221*x2)+x1*(141840+15973*x2) < 42786", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C6" Description "Example C6". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; End. Problem -1/10 <= x1 & x1 <= 1/10 & -1/10 <= x2 & x2 <= 1/10 -> [ {x1' = -2*x1 + x1^2 + x2, x2' = x1 - 2*x2 + x2^2 & -1 <= x1 & x1 <= 1 & -1 <= x2 & x2 <= 1}@invariant(x1*(189+111470000*x1)+x2*(189+111470000*x2) < 43801000) ] !( 1/2 <= x1 & x1 <= 1 & 1/2 <= x2 & x2 <= 1 ) End. Tactic "Scripted proof" implyR(1) ; dC("x1*(189+111470000*x1)+x2*(189+111470000*x2) < 43801000", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C7" Description "Example C7". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; End. Problem -3/2 <= x1 & x1 <= -1/2 & -3/2 <= x2 & x2 <= -1/2 -> [ {x1' = -x1 + x1*x2, x2' = -x2 & -2 <= x1 & x1 <= 2 & -2 <= x2 & x2 <= 2}@invariant(x2 < 0) ] !( -1/2 <= x1 & x1 <= 1/2 & 1/2 <= x2 & x2 <= 3/2 ) End. Tactic "Scripted proof" implyR(1) ; dC("x2 < 0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C8" Description "Example C8". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; End. Problem -1/4 <= x1 & x1 <= 1/4 & 3/4 <= x2 & x2 <= 3/2 -> [ {x1' = -x1 + 2*x1^2*x2, x2' = -x2 & -2 <= x1 & x1 <= 2 & -2 <= x2 & x2 <= 2}@invariant(x1*x2 < 1) ] !( 1 <= x1 & x1 <= 2 & 1 <= x2 & x2 <= 2 ) End. Tactic "Scripted proof" implyR(1) ; dC("x1*x2 < 1", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Papachristodoulou Prajna 2002: Example 2 (Chemical Oscillator)" Citation "Antonis Papachristodoulou, Stephen Prajna. On the Construction of Lyapunov Functions using the Sum of Squares Decomposition. 2002.". Link "https://doi.org/10.1109/CDC.2002.1184414". Definitions Real a, b; End. ProgramVariables Real u, v; End. Problem a >= 0.25 & b>= 0 & u = 0.01 & v = 0 -> [{u' = a - u + u^2*v, v' = b - u^2*v }/* @invariant(origin is a stable equilibrium with these values of a and b) */ ]!(u^2 + v^2 > 10) End. End. ArchiveEntry "Benchmarks/Nonlinear/Prajna PhD Thesis 2-4-1 Page 31" Description "Page 31". Citation "Prajna, Stephen (2005) Optimization-based methods for nonlinear and hybrid systems verification; Dissertation (Ph.D.), California Institute of Technology.". Link "http://resolver.caltech.edu/CaltechETD:etd-05272005-144358". ProgramVariables Real x; Real y; End. Problem (-3/2 + x)^2 + y^2 <= 1/4 -> [ {x'=x, y'=-x+x^3/3-y} @invariant(x>=0) ] !((1 + x)^2 + (1 + y)^2 <= 4/25) End. Tactic "Scripted proof" implyR('R=="(-3/2+x)^2+y^2<=1/4->[{x'=x,y'=-x+x^3/3-y}](!(1+x)^2+(1+y)^2<=4/25)"); dC("x>=0", 'R=="[{x'=x,y'=-x+x^3/3-y}](!(1+x)^2+(1+y)^2<=4/25)"); <( "Use": dW('R=="[{x'=x,y'=-x+x^3/3-y&true&x>=0}](!(1+x)^2+(1+y)^2<=4/25)"); QE, "Show": dbx('R=="[{x'=x,y'=-x+x^3/3-y}]x>=0") ) End. Tactic "Automated proof" autoClose End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 1" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem (-3)<=x & x<=(-2) & (-3)<=y&y<=(-2) -> [{x'=4 + 21*x - 7*y + 42*x^2 - 24*x*y + 4*y^2 + 27*x^3 - 9*x^2*y + 6*x^4, y'=12 + 71*x -21*y + 150*x^2 -80*x*y + 12*y^2 + 99*x^3 - 39*x^2*y + 2*x*y^2 + 18*x^4} @invariant(3+x>=0, 3+y>=0, 4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y, 1+x*(3+x)>y, 1+3*x*(2+x)>2*y, 2+3*x < y, x < 0, y < 0) ]!(x >= 0 | y >= 0) End. Tactic "Scripted proof" implyR('R=="(-3)<=x&x<=(-2)&(-3)<=y&y<=(-2)->[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4}](!(x>=0|y>=0))"); dC("3+x>=0", 'R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4}](!(x>=0|y>=0))"); <( "Use": dC("3+y>=0", 'R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&true&3+x>=0}](!(x>=0|y>=0))"); <( "Use": dC("4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y", 'R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&(true&3+x>=0)&3+y>=0}](!(x>=0|y>=0))"); <( "Use": dC("1+x*(3+x)>y", 'R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y}](!(x>=0|y>=0))"); <( "Use": dC("1+3*x*(2+x)>2*y", 'R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&(((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y}](!(x>=0|y>=0))"); <( "Use": dC("2+3*x < y", 'R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&((((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y)&1+3*x*(2+x)>2*y}](!(x>=0|y>=0))"); <( "Use": dC("x < 0", 'R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&(((((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y)&1+3*x*(2+x)>2*y)&2+3*x < y}](!(x>=0|y>=0))"); <( "Use": dC("y < 0", 'R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&((((((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y)&1+3*x*(2+x)>2*y)&2+3*x < y)&x < 0}](!(x>=0|y>=0))"); <( "Use": dW('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&(((((((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y)&1+3*x*(2+x)>2*y)&2+3*x < y)&x < 0)&y < 0}](!(x>=0|y>=0))"); chaseAt('R=="!(x>=0|y>=0)"); propClose, "Show": ODEinv('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&((((((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y)&1+3*x*(2+x)>2*y)&2+3*x < y)&x < 0}]y < 0") ), "Show": ODEinv('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&(((((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y)&1+3*x*(2+x)>2*y)&2+3*x < y}]x < 0") ), "Show": dbx('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&((((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y)&1+3*x*(2+x)>2*y}]2+3*x < y") ), "Show": dbx('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&(((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y)&1+x*(3+x)>y}]1+3*x*(2+x)>2*y") ), "Show": dbx('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&((true&3+x>=0)&3+y>=0)&4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y}]1+x*(3+x)>y") ), "Show": ODEinv('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&(true&3+x>=0)&3+y>=0}]4+3*x*(1+x)*(7+x*(7+2*x))+4*y^2>(7+3*x*(8+3*x))*y") ), "Show": ODEinv('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4&true&3+x>=0}]3+y>=0") ), "Show": ODEinv('R=="[{x'=4+21*x-7*y+42*x^2-24*x*y+4*y^2+27*x^3-9*x^2*y+6*x^4,y'=12+71*x-21*y+150*x^2-80*x*y+12*y^2+99*x^3-39*x^2*y+2*x*y^2+18*x^4}]3+x>=0") ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 1 (Variant)" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem (1 + x)^2 + (2 + y)^2 <= 1/4 -> [{x'=4 + 21*x + 42*x^2 + 27*x^3 + 6*x^4 - 7*y - 24*x*y - 9*x^2*y + 4*y^2, y'=12 + 71*x + 150*x^2 + 99*x^3 + 18*x^4 - 21*y - 80*x*y - 39*x^2*y + 12*y^2 + 2*x*y^2} ](-2 + x)^2 + (2 + y)^2 > 1/4 End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 2" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem (x + 2)^2 + (y + 2)^2 <= 5 -> [{x'=x+2*y-y^2, y'=-y+y^2}@invariant(x+y < 0, x < ((-2)+y)*y)]2*x+y < 0 End. Tactic "Scripted proof" implyR('R=="(x+2)^2+(y+2)^2<=5->[{x'=x+2*y-y^2,y'=-y+y^2}]2*x+y < 0"); dC("x+y < 0", 'R=="[{x'=x+2*y-y^2,y'=-y+y^2}]2*x+y < 0"); <( "Use": dC("x < ((-2)+y)*y", 'R=="[{x'=x+2*y-y^2,y'=-y+y^2&true&x+y < 0}]2*x+y < 0"); <( "Use": ODEinv('R=="[{x'=x+2*y-y^2,y'=-y+y^2&(true&x+y < 0)&x < ((-2)+y)*y}]2*x+y < 0"), "Show": ODEinv('R=="[{x'=x+2*y-y^2,y'=-y+y^2&true&x+y < 0}]x < ((-2)+y)*y") ), "Show": dbx('R=="[{x'=x+2*y-y^2,y'=-y+y^2}]x+y < 0") ) End. Tactic "Automated proof" autoClose End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 2 (Variant)" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem (x - 4)^2 + y^2 <= 1 -> [{x'=x+2*y-y^2, y'=-y+y^2}@invariant(y<=1, 273630+y*((-32671)+81001*y) < 123190*x)]!(x < 2 | y > 1) End. Tactic "Scripted proof" implyR(1) ; dC("y<=1", 1) ; <( dC("273630+y*((-32671)+81001*y) < 123190*x", 1) ; <( dW(1) ; QE, barrier(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 3" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem (x+3)^2+(y+3)^2<=1 -> [{x'=3*x+y^2, y'=5*y & -6<=x & x<= 6 & -6 <= y & y<=6}@invariant(63232*x^3+x^2*((-66727)+176350*y)+10*x*(42940+y*(55669+25688*y))+10*(808140+y*(289690+9*y*(9466+1595*y))) < 0)]x + y < -2 End. Tactic "Scripted proof" implyR(1) ; dC("63232*x^3+x^2*((-66727)+176350*y)+10*x*(42940+y*(55669+25688*y))+10*(808140+y*(289690+9*y*(9466+1595*y))) < 0", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 4" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem y >= 2.5 | x >= 0 -> [{x'=6*x^2 - 6*x*y + 4*y^2 + 3*x^3 - 9*x^2*y + 6*x^4, y'=-6*x*y + 10*y^2 + 27*x^3 - 39*x^2 + 2*x*y^2 + 18*x^4} ](x + 3)^2 + (y + 2)^2 > 3 End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 5" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem (x + 3)^2 + (y + 3)^2 <= 1 -> [{x'=x+y+x^2, y'=x*(1+y)}@invariant(1+y < 0, 70030000+331*x^2+5*y*(4429100+61943*y) < 50*x*((-629110)+27787*y))] x+y < -2 End. Tactic "Scripted proof" implyR(1) ; dC("1+y < 0", 1) ; <( dC("70030000+331*x^2+5*y*(4429100+61943*y) < 50*x*((-629110)+27787*y)", 1) ; <( dW(1) ; QE, barrier(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 5 (Variant 1)" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem (x - 4)^2 + (y - 4)^2 <= 1 -> [{x'=x+y+x^2, y'=x*(1+y)}@invariant(1+y>0, x^2 < y*(x+y), 387150000+426*x^2+85*y < 36465000*x*y)](x - 2)^2 + (y - 2)^2 > 3 End. Tactic "Scripted proof" implyR(1) ; dC("1+y>0", 1) ; <( dC("x^2 < y*(x+y)", 1) ; <( dC("387150000+426*x^2+85*y < 36465000*x*y", 1) ; <( dW(1) ; QE, barrier(1) ), dbx(1) ), dbx(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Ferragut Giacomini 2010: Example 5 (Variant 2)" Citation "Antoni Ferragut, Hector Giacomini: A New Algorithm for Finding Rational First Integrals of Polynomial Vector Fields; Qual. Theory Dyn. Syst. (2010)". ProgramVariables Real x; Real y; End. Problem (x + 1)^2 + (y - 4)^2 <= 1 -> [{x'=x+y+x^2, y'=x*(1+y)}@invariant(1+y>0, 23921*x+18696*y+2089*x*y>5916)](x + 2)^2 + (y + 2)^2 > 2 End. Tactic "Scripted proof" implyR(1) ; dC("1+y>0", 1) ; <( dC("23921*x+18696*y+2089*x*y>5916", 1) ; <( dW(1) ; QE, barrier(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C1" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C1". ProgramVariables Real x; Real y; Real u1, u2, u3, u4; End. Problem (x-1.5)^2+y^2<=0.25 & 0.99<=u1&u1<=1.01 & 0.96<=u2&u2<=1.04 & 0.32<=u3&u3<=0.347 & 0.98<=u4&u4<=1.02 -> [{x'=u1*y, y'=-u2*x+u3*x^3-u4*y & -2<=x&x<=2 & -2<=y&y<=2} ]!(x+1)^2+(y+1)^2<=0.16 End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C1 (Nonparametric)" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C1". ProgramVariables Real x; Real y; Real u1, u2, u3, u4; End. Problem (x-1.5)^2+y^2<=0.25 & u1=1 & u2=1 & u3=0.33 & u4=1 -> [{x'=u1*y, y'=-u2*x+u3*x^3-u4*y & -2<=x&x<=2 & -2<=y&y<=2} ]!(x+1)^2+(y+1)^2<=0.16 End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C2" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C2". ProgramVariables Real x; Real y; Real u1, u2; End. Problem (x-1)^2+y^2<=0.04 & -1.1<=u1&u1<=-0.9 & 2.98<=u2&u2<=3.02 -> [{x'=u1*y-3/2*x^2-1/2*x^3, y'=u2*x-y & -2<=x&x<=2 & -2<=y&y<=2} ]!(x+1.8)^2+y^2<=0.16 End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C2 (Nonparametric)" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C2". ProgramVariables Real x; Real y; Real u1, u2; End. Problem (x-1)^2+y^2<=0.04 & u1=-1 & u2=3 -> [{x'=u1*y-3/2*x^2-1/2*x^3, y'=u2*x-y & -2<=x&x<=2 & -2<=y&y<=2} @invariant(x*((-26090)+x*(34696+12539*x))+38464*y < 61620) ]!(x+1.8)^2+y^2<=0.16 End. Tactic "Scripted proof" implyR(1); dC("x*((-26090)+x*(34696+12539*x))+38464*y < 61620", 1); <( "Use": dW(1); QE, "Show": barrier(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Djaballah Chapoutot Kieffer Bouissou 2017: Example 3" Description "Example 3, p; 293". Citation "Adel Djaballah, Alexandre Chapoutot, Michel Kieffer, Olivier Bouissou; Construction of parametric barrier functions for dynamical systems using interval analysis; Automatica 78 (2017) 287–296.". Link "https://doi.org/10.1016/j.automatica.2016.12.013". ProgramVariables Real x1, x2; End. Problem (x1+1.125)^2 + (x2-0.625)^2 - 0.0125 <= 0 -> [{x1'=-x1+x1*x2, x2'=-x2}@invariant(x1 < 0) ]!((x1-0.875)^2 + (x2-0.125)^2 - 0.0125 <= 0) End. Tactic "Scripted proof" implyR(1) ; dC("x1 < 0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Djaballah Chapoutot Kieffer Bouissou 2017: Example 5" Description "Example 5, p; 293". Citation "Adel Djaballah, Alexandre Chapoutot, Michel Kieffer, Olivier Bouissou; Construction of parametric barrier functions for dynamical systems using interval analysis; Automatica 78 (2017) 287–296.". Link "https://doi.org/10.1016/j.automatica.2016.12.013". Definitions Real d; End. ProgramVariables Real x1, x2; End. Problem (x1-1.5)^2 + x2^2 - 0.25 <= 0 & 0.9<=d&d<=1.1 -> [{x1'=x2, x2'=-x1+d/3*x1^3 - x2} ]!((x1+0.8)^2 + (x2+1)^2 - 0.25 <= 0) End. End. /* 3D Problems */ ArchiveEntry "Benchmarks/Nonlinear/3D Lotka Volterra (I)" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". Definitions Real invcluster(Real x, Real y, Real z, Real u3, Real u4) = ( u3*x+u3*y+u3*z+u4 ); End. ProgramVariables Real x; Real y; Real z; End. Problem x=1 & y=1 & z=1 -> [{ x'=x*y-x*z, y'=y*z-y*x, z'=z*x-z*y }@invariant(x>0, y>0, z>0) ](x + 2*y + z^3 > 0) End. Tactic "Scripted proof" implyR(1) ; dC("x>0", 1) ; <( dC("y>0", 1) ; <( dC("z>0", 1) ; <( dW(1) ; QE, dbx(1) ), dbx(1) ), dbx(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; cut("\exists u3 \exists u4 (u3^2+u4^2!=0 & invcluster(x,y,z,u3,u4)=0)") ; <( existsL('Llast)*2 ; dC("invcluster(x,y,z,u3,u4)=0", 1) ; doall(ODEinv(1)) ; done , hideR(1) ; QE ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/3D Lotka Volterra (II)" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". Definitions Real invcluster(Real x, Real y, Real z, Real u5, Real u10, Real u16, Real u19, Real u20) = ( u5*x*y*z+u10*x^3+3*u10*x^2*y+3*u10*x^2*z+3*x*y^2*u10+3*x*z^2*u10+u10*y^3+ 3*u10*y^2*z+3*u10*y*z^2+u10*z^3+u16*x^2+2*u16*x*y+2*u16*x*z+ u16*y^2+2*u16*y*z+u16*z^2+u19*x+u19*y+u19*z+u20 ); End. ProgramVariables Real x; Real y; Real z; End. Problem x=-1 & y=-1 & z=-1 -> [{ x'=x*y-x*z, y'=y*z-y*x, z'=z*x-z*y }@invariant(x<0, y<0, z<0) ](x^5 + 12*y + z^3 < 0) End. Tactic "Scripted proof" implyR(1) ; dC("x < 0", 1) ; <( dC("y < 0", 1) ; <( dC("z < 0", 1) ; <( dW(1) ; QE, dbx(1) ), dbx(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/3D Lotka Volterra (III)" Citation "Sriram Sankaranarayanan. Automatic Invariant Generation for Hybrid Systems Using Ideal Fixed Points". ProgramVariables Real x; Real y; Real z; End. Problem x=1 & y=1 & z=-1 -> [{ x'=x*y-x*z, y'=y*z-y*x, z'=z*x-z*y }@invariant(x>0, y>0, z<0) ](x + y - z > -2) End. Tactic "Scripted proof" implyR(1) ; dC("x>0", 1) ; <( dC("y>0", 1) ; <( dC("z < 0", 1) ; <( dW(1) ; QE, dbx(1) ), dbx(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Alongi Nelson Ex_4_1_9 page 143" Description "Ex 4.1.9 Page 143". Citation "John M. Alongi and Gail S. Nelson. Recurrence and Topology". ProgramVariables Real x; Real y; Real z; End. Problem x = 1 & y = 0 & z = 0 -> [{x'=x*z , y'=y*z , z'=-x^2-y^2 & x^2+y^2+z^2=1}@invariant(x+y>0)] !((x > -1 -> x^2 > 2) | z > 1) /* Known invariant: (x <= 1 & z <= 0) */ End. Tactic "Scripted proof" implyR(1) ; dC("x+y>0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; dC("x<=1&z<=0", 1) ; <( ODEinv(1), ODEinv(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Constraint-based Example 8 (Phytoplankton Growth)" Citation "Sumit Gulwani and Ashish Tiwari. Constraint-based Approach for Analysis of Hybrid Systems". ProgramVariables Real x1; Real x2; Real x3; End. Problem x1 = 0 & x2 = 0 & x3 = 0 -> [ {x1'=1 - x1 - (x1*x2)/4, x2'=x2*(-1 + 2*x3), x3'=x1/4 - 2*x3^2 }@invariant(x2=0, x1<=5) ] (x1 <= 5 & x2 <= 5 & x3 <= 5) End. Tactic "Scripted proof" implyR(1) ; dC("x2=0", 1) ; <( dC("x1<=5", 1) ; <( boxAnd(1) ; andR(1) ; <( dW(1) ; prop, boxAnd(1) ; andR(1) ; <( dW(1) ; QE, dbx(1) ) ), dbx(1) ), dbx(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Invariant 3-dim sphere" ProgramVariables Real x; Real y; Real z; End. Problem x = 1/4 & y = 1/8 & z = 1/10 -> [ {x'=x^2-x*(x^3+y^3+z^3), y'=y^2-y*(x^3+y^3+z^3), z'=z^2-z*(x^3+y^3+z^3)}@invariant(x^2+y^2+z^2 < 1) ] !(x > 10 | y > 5 | z <= -20) End. Tactic "Scripted proof" implyR(1) ; dC("x^2+y^2+z^2 < 1", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Invariant Clusters Example 4" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". ProgramVariables Real x; Real y; Real z; End. Problem x=1 & y=2 & z=3 -> [ {x'=y*z, y'=x*z, z'=x*y }@invariant(5+y^2=z^2) ] !(x=5 & y^2=27 & z^2=34) End. Tactic "Scripted proof" implyR(1) ; dC("5+y^2=z^2", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; cut("\exists u0 \exists u5 \exists u6 (u0^2+u5^2+u6^2!=0 & invcluster(x,y,z,u0,u5,u6)=0)") ; <( existsL('Llast)*3 ; dC("invcluster(x,y,z,u0,u5,u6)=0", 1) ; doall(ODEinv(1)) ; done , hideR(1) ; QE ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Invariant Clusters Example 5" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". ProgramVariables Real x; Real y; Real z; End. Problem x=1 & y=2 & z=3 -> [ { x'=y*z, y'=x*z, z'=x*y }@invariant(5+y^2=z^2) ] !(x=5 & y^2=27 & z^2=34) End. Tactic "Scripted proof" implyR(1) ; dC("5+y^2=z^2", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Looping Particle" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". Definitions Real g; Real r; Real invcluster(Real x, Real y, Real omega, Real u0, Real u2, Real u5) = ( u5*x^2+u5*y^2+u2*omega^2+2*u2*g/r^2*y+u0 ); End. ProgramVariables Real x; Real y; Real omega; End. Problem x=2 & y=0 & r=2 -> [{ x'=-y*omega, y'=x*omega, omega'=-g/r^2*x }@invariant(x^2+y^2>=4) ]2*x^2+y^2 > 3 End. Tactic "Scripted proof" implyR(1) ; dC("x^2+y^2>=4", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; dC("x^2+y^2=r^2", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (3)" implyR(1) ; cut("\exists u0 \exists u2 \exists u5 (u0^2+u2^2+u5^2!=0 & invcluster(x,y,omega,u0,u2,u5)=0)") ; <( existsL('Llast)*3 ; dC("invcluster(x,y,omega,u0,u2,u5)=0", 1) ; doall(ODEinv(1)) ; done , hideR(1) ; QE ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Shimizu Morioka System" ProgramVariables Real x; Real y; Real z; End. Problem x = 5 & y = 3 & z = -4 -> [{x'=y, y'=x-y-x*z, z'=x^2-z}@invariant(z>=-5)]!(z < 0 & z^2 > 26+x^2) End. Tactic "Scripted proof" implyR(1) ; dC("z>=-5", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C2" Description "Example C2". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; Real x3; End. Problem -0.25 <= x1 & x1 <= 0.75 & -0.25 <= x2 & x2 <= 0.75 & -0.75 <= x3 & x3 <= 0.25 -> [ {x1' = -x2, x2' = -x3, x3' = -x1 - 2*x2 - x3 + x1^3 & -2 <= x1 & x1 <= 2 & -2 <= x2 & x2 <= 2 & -2 <= x3 & x3 <= 2}@invariant(7*x1*(425300+3161*x1^2) < 5*(909080+23721*x2+295290*x3)) ] !( 1 <= x1 & x1 <= 2 & -2 <= x2 & x2 <= -1 & -2 <= x3 & x3 <= -1 ) End. Tactic "Scripted proof" implyR(1) ; dC("7*x1*(425300+3161*x1^2) < 5*(909080+23721*x2+295290*x3)", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C3" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C3". ProgramVariables Real x, y, z; Real u1, u2, u3; End. Problem (x-1.5)^2+y^2+z^2<=0.0625 & -1.1<=u1&u1<=-1 & 0.9<=u2&u2<=1 & 4.7<=u3&u3<=4.8 -> [{x'=u1*x+y-z, y'=-x*(z+1)-u2*y, z'=-0.77*x-u3*z & -2<=x&x<=2 &-2<=y&y<=2 & -2<=z&z<=2} @invariant(2.7699+2.7025*x+1.4255*y-1.0938*z+0.95692*x^2+0.29671*y*x+0.72331*y^2-0.62314*x*z+0.26337*z*y-0.17821*z^2>=0) ]!(x+1)^2+(y+1)^2+(z-1)^2<=0.0625 End. /* Proving invariant stuck */ End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C3 (Nonparametric)" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C3". ProgramVariables Real x, y, z; Real u1, u2, u3; End. Problem (x-1.5)^2+y^2+z^2<=0.0625 & u1=-1 & u2=1 & u3=4.75 -> [{x'=u1*x+y-z, y'=-x*(z+1)-u2*y, z'=-0.77*x-u3*z & -2<=x&x<=2 &-2<=y&y<=2 & -2<=z&z<=2} @invariant(12583*x+97936*z < 60051) ]!(x+1)^2+(y+1)^2+(z-1)^2<=0.0625 End. Tactic "Scripted proof" implyR(1) ; dC("12583*x+97936*z < 60051", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C4" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C4". ProgramVariables Real x1, x2, x3; Real u1, u2, u3, u4; End. Problem 0<=x1&x1<=0.5 & 0<=x2&x2<=0.5 & -0.5<=x3&x3<=0 & -0.9<=u1&u1<=-0.8 & -1.2<=u2&u2<=-1.1 & -1.2<=u3&u3<=-1 & 2.1<=u4&u4<=2.4 -> [{x1'=u1*x2, x2'=u2*x3, x3'=u3*x1-u4*x2-x3+x1^3 & -2<=x1&x1<=2 & -2<=x2&x2<=2 & -2<=x3&x3<=2} /* Not implied by precondition @invariant(0.289+0.1*x1*x2-0.2*x1*x3-0.34*x2*x3+0.87*x2+0.55*x3-1.12*x1+0.23*x1^2+0.4*x2^2+0.02*x3^2>=0) */ ]!(0.5<=x1&x1<=2 & -2<=x2&x2<=-1.5 & -2<=x3&x3<=-1.5) End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C4 (Nonparametric)" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C4". ProgramVariables Real x1, x2, x3; Real u1, u2, u3, u4; End. Problem 0<=x1&x1<=0.5 & 0<=x2&x2<=0.5 & -0.5<=x3&x3<=0 & u1=-0.85 & u2=-1.15 & u3=-1.16 & u4=2.2 -> [{x1'=u1*x2, x2'=u2*x3, x3'=u3*x1-u4*x2-x3+x1^3 & -2<=x1&x1<=2 & -2<=x2&x2<=2 & -2<=x3&x3<=2} @invariant(722620*x1+17021*x1^3 < 890220+33020*x2+318530*x3) ]!(0.5<=x1&x1<=2 & -2<=x2&x2<=-1.5 & -2<=x3&x3<=-1.5) End. Tactic "Scripted proof" implyR(1) ; dC("722620*x1+17021*x1^3 < 890220+33020*x2+318530*x3", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.2" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems;". ProgramVariables Real x1, x2, x3; End. Problem x1^2 + x2^2 + x3^2 >= 5 -> [{x1'=2*x1+x2, x2'=x1+3*x2-x3, x3'=-x1+2*x2+3*x3 }]!(x1^2+x2^2+x3^2 < 1) End. Tactic "Scripted proof" implyR(1) ; dbx(1) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.4" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems;". ProgramVariables Real x1, x2, x3; End. Problem x2 < x1 & x2 < x3 & x3 > 0 & x3 < 12 -> [{x1'=4*x1-5*x2+2*x3, x2'=5*x1-7*x2+3*x3, x3'=6*x1-9*x2+4*x3}@invariant(x1+x3>=2*x2) ] !(x1 < 0.5 & x3 < 0.5 & x2 > 1) End. Tactic "Scripted proof" implyR(1) ; dC("x1+x3>=2*x2", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.5 Variant 1" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems;". ProgramVariables Real x1, x2, x3; End. Problem ((x2 >= 0 & 2*x2 < x3 & 3*x2 < x1) | (x2 <= 0 & x1 >= -0.4 & x3 > 0.5)) -> [{x1'=4*x1-x2, x2'=3*x1+x2-x3, x3'=x1+x3}@invariant(x1+x3>x2) ] !(4*x1 < x2 & x3 < x1 & x2 > 0.5) End. Tactic "Scripted proof" implyR(1) ; dC("x1+x3>x2", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.5 Variant 2" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems;". ProgramVariables Real x1, x2, x3; End. Problem (x3 > 1 & x1 > (x1 - x3)^2 & x3 > x2) -> [{x1'=4*x1-x2, x2'=3*x1+x2-x3, x3'=x1+x3}@invariant((x1-x3)^2-2*x3*(x1-x2+x3) < 0) ] !(x3 < 0 & x1 - x2 + x3 > 0) End. Tactic "Scripted proof" implyR(1) ; dC("(x1-x3)^2-2*x3*(x1-x2+x3) < 0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.5 Variant 3" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems;". ProgramVariables Real x1, x2, x3; End. Problem x1 > 0 & x2 > 0 & x3 > 0 & x1 > x2 & x3 > x1 -> [{x1'=4*x1-x2, x2'=3*x1+x2-x3, x3'=x1+x3}@invariant((x1-x3)^2-2*x3*(x1-x2+x3) < (x1-x2+x3)^2) ] !(x2 = x3 & x3 > 5 & x1 < 1/5) End. Tactic "Scripted proof" implyR(1) ; dC("2*x2*(x1+2*x3) < x2^2+2*x3*(3*x1+x3)", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; dC("(x1-x3)^2-2*x3*(x1-x2+x3) < (x1-x2+x3)^2", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Djaballah Chapoutot Kieffer Bouissou 2017: Example 7" Description "Example 7, p; 293". Citation "Adel Djaballah, Alexandre Chapoutot, Michel Kieffer, Olivier Bouissou; Construction of parametric barrier functions for dynamical systems using interval analysis; Automatica 78 (2017) 287–296.". Link "https://doi.org/10.1016/j.automatica.2016.12.013". ProgramVariables Real x1, x2, x3; End. Problem (x1+14.5)^2 + (x2+14.5)^2 + (x3-12.5)^2 - 0.25 <= 0 -> [{x1'=10*(x2-x1), x2'=x1*(28-x3)-x2, x3'=x1*x2-8/3*x3} ]!((x1+16.5)^2 + (x2+14.5)^2 + (x3-2.5)^2 - 0.25 <= 0) End. End. ArchiveEntry "Benchmarks/Nonlinear/Llibre Zhang 2002: Lorenz System (Parametric)" Citation "Jaume Llibre, Xiang Zhang. On the invariant algebraic surfaces of the Lorenz systems. J. Math. Phys. 43, 1622 (2002)". Link "https://doi.org/10.1063/1.1435078". Definitions Real b, r, s; End. ProgramVariables Real x, y, z1; End. Problem ((s = -z1 | (s > 0.5 & z1 < -0.5 & x > 1)) & b = 2*s) -> [{x'=s*(y-x), y'=r*x-y-x*z1, z1'=-b*z1+x*y }@invariant((x^2 - 2*s*z1) >= 0) ]!((s > z1 | s > 2*z1) & z1 > x & x > 1) End. Tactic "Scripted proof" implyR(1) ; dC("x^2-2*s*z1>=0", 1) ; <( dW(1) ; QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Llibre Zhang 2002: Lorenz System (p. 1623 b=2s Variant s=1 r=1)" Citation "Jaume Llibre, Xiang Zhang. On the invariant algebraic surfaces of the Lorenz systems. J. Math. Phys. 43, 1622 (2002)". Link "https://doi.org/10.1063/1.1435078". Definitions Real b, r, s; End. ProgramVariables Real x, y, z2; End. Problem z2 > 5*x & x > 0 & x < 4 & b=2 & s=1 & r=1 -> [{x'=s*(y-x), y'=r*x-y-x*z2, z2'=-b*z2+x*y }@invariant(x^2 - 2*s*z2 <= 0) ]!((s <=1 & s >= -1) & (z2 <= 1 & z2 >= -1) & x > 1.8) End. Tactic "Scripted proof" implyR(1) ; dC("x^2 < 2*z2", 1) ; <( dW(1) ; QE, ODEinv(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Llibre Zhang 2002: Lorenz System (p. 1623 b=0 s=0.33)" Citation "Jaume Llibre, Xiang Zhang. On the invariant algebraic surfaces of the Lorenz systems. J. Math. Phys. 43, 1622 (2002)". Link "https://doi.org/10.1063/1.1435078". Definitions Real b, r, s; End. ProgramVariables Real x, y, z3; End. Problem x=y & r < -1 & z3>x^2 & b=0 & s=1/3 -> [{x'=s*(y-x), y'=r*x-y-x*z3, z3'=-b*z3+x*y }@invariant(-r()*x^2+1/3*y^2+2/3*x*y+x^2*z3-3/4*x^4>=0) ]!(y < 0 & z3 < -1 & r < 0 & z3 < r & x > -y) End. Tactic "Scripted proof" implyR(1) ; dC("-r()*x^2+1/3*y^2+2/3*x*y+x^2*z3-3/4*x^4>=0", 1) ; <( dW(1) ; QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Llibre Zhang 2002: Lorenz System (p. 1623 b=0 s=0.33 Variant r=1)" Citation "Jaume Llibre, Xiang Zhang. On the invariant algebraic surfaces of the Lorenz systems. J. Math. Phys. 43, 1622 (2002)". Link "https://doi.org/10.1063/1.1435078". Definitions Real b, r, s; End. ProgramVariables Real x, y, z4; End. Problem z4 > 1 & x > 0 & y > 3*x^2 & b=0 & s=1/3 & r=1 -> [{x'=s*(y-x), y'=r*x-y-x*z4, z4'=-b*z4+x*y }@invariant(-r*x^2 + 1/3*y^2 + 2/3*x*y + x^2*z4 - 3/4*x^4 >= 0) ]!(x > 1 & y > 0 & z4 < 0 & -z4 > y^2 + y) End. Tactic "Scripted proof" implyR(1) ; dC("-r()*x^2+1/3*y^2+2/3*x*y+x^2*z4-3/4*x^4>=0", 1) ; <( dW(1) ; QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Llibre Zhang 2002: Lorenz System (p. 1623 b=1 r=0)" Citation "Jaume Llibre, Xiang Zhang. On the invariant algebraic surfaces of the Lorenz systems. J. Math. Phys. 43, 1622 (2002)". Link "https://doi.org/10.1063/1.1435078". Definitions Real b, r, s; End. ProgramVariables Real x, y, z5; End. Problem 2*y^2 + z5^2 <= 0.5 & b=1 & r=0 -> [{x'=s*(y-x), y'=r*x-y-x*z5, z5'=-b*z5+x*y }@invariant(y^2+z5^2<=1) ] (y^2 + 2*z5^2 <= 5) End. Tactic "Scripted proof" implyR(1) ; dC("y^2+z5^2<=1", 1) ; <( dW(1) ; QE, ODEinv(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Llibre Zhang 2002: Lorenz System (p. 1623 b=1 r=0 Variant s=1)" Citation "Jaume Llibre, Xiang Zhang. On the invariant algebraic surfaces of the Lorenz systems. J. Math. Phys. 43, 1622 (2002)". Link "https://doi.org/10.1063/1.1435078". Definitions Real b, r, s; End. ProgramVariables Real x, y, z6; End. Problem y^2 + 2*z6^2 <= 1 & b=1 & r=0 & s=1 -> [{x'=s*(y-x), y'=r*x-y-x*z6, z6'=-b*z6+x*y }@invariant(y^2+z6^2 <= 2) ](y^2 + 0.5*z6^2 <= 3) End. Tactic "Scripted proof" implyR(1) ; dC("y^2+z6^2<=2", 1) ; <( dW(1) ; QE, ODEinv(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; dC("1047*(y^2+z6^2) < 1979", 1) ; <( dW(1) ; QE, barrier(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. /* Higher-D Problems */ /* 4 D */ ArchiveEntry "Benchmarks/Nonlinear/Coupled Spring-Mass System (I)" Citation "Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang, Thomas A. Henzinger. Invariant Clusters for Hybrid Systems; CoRR abs/1605;01450 (2016)". Definitions Real m1; Real m2; Real k1; Real k2; Real k; Real u1; Real u8; Real u10; Real invcluster(Real x1, Real x2, Real v1, Real v2) = ( u8*v1*v2+k2*x1*x2*(m1*u8-2*m2*u10)/(m1*m2) + u10*v1^2+u1 + 1/2*v2^2*(k1*m2*u8-k2*m1*u8+k2*m2*u8+2*k2*m2*u10)/(k2*m1) + 1/2*(2*k1*m2*u10-k2*m1*u8+2*k2*m2*u10)*x1^2/(m1*m2) + 1/2*(k1*m2*u8-k2*m1*u8+2*k2*m2*u10)*x2^2/(m1*m2) ); End. ProgramVariables Real x1; Real x2; Real v1; Real v2; End. Problem x1=0 & v1=0 & x2=7/8 & v2=0 & k1=-1 & k2=-1 & k=-1 & m1=5 & m2=1 & u10=0 & u1=0 & u8=320/49 -> [{ x1'=v1, v1'=-k1/m1*x1-k2/m1*(x1-x2), x2'=v2, v2'=-k2/m2*(x2-x1) }@invariant(v1*v2+(-3)/10*v2^2+1/2*x1^2+(-1)*x1*x2+2/5*x2^2>=358/1169) ]!invcluster(x1,x2,v1,v2) < -v1^2 End. Tactic "Scripted proof" implyR(1) ; dC("v1*v2+(-3)/10*v2^2+1/2*x1^2+(-1)*x1*x2+2/5*x2^2>=358/1169", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; dC("invcluster(x1,x2,v1,v2)>=0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Coupled Spring-Mass System (II)" Citation "Sriram Sankaranarayanan. Automatic Invariant Generation for Hybrid Systems Using Ideal Fixed Points". Definitions Real k; End. ProgramVariables Real x1; Real x2; Real v1; Real v2; End. Problem x1=0 & x2=0 & v1=1 & v2=-1 -> [{ x1'=v1, x2'=v2, v1'=-k*x1-k/5*(x1-x2), v2'=k*(x1-x2) } ](25*v1^2+60*v1*v2+11*v2^2+50*k*x1*x2+5*k*x2^2 > -25 - v1^2 - v2^2) /* Invariants from paper: 576+1200*v1^2+625*v1^4+2880*v1*v2+3000*v1^3*v2+528*v2^2+4150*v1^2*v2^2+1320*v1*v2^3+121*v2^4-1860*k*x2^2+2750*k*v1^2*x2^2+1600*k*v1*v2*x2^2+710*k*v2^2*x2^2+525*k^2*x2^4 = 0, 240*x1+250*v1^2*x1+600*v1*v2*x1+110*v2^2*x1+396*x2-525*v1^2*x2-260*v1*v2*x2-131*v2^2*x2-105*k*x2^3 = 0, 24+25*v1^2+60*v1*v2+11*v2^2+50*k*x1*x2+5*k*x2^2 = 0, -21+25*v1^2+10*v1*v2+6*v2^2+25*k*x1^2+5*k*x2^2 = 0 */ End. End. ArchiveEntry "Benchmarks/Nonlinear/Damped Mathieu System" Citation "James Kapinski, Jyotirmoy V. Deshmukh, Sriram Sankaranarayanan, and Nikos Arechiga. 2014. Simulation-guided Lyapunov analysis for hybrid dynamical systems; In Proceedings of the 17th International Conference on Hybrid systems: computation and control (HSCC '14). ACM, New York, NY, USA, 133-142. DOI=http://doi.org/10.1145/2562059.2562139". Definitions Real LyapunovCandidate(Real x1, Real x2) = ( 98*x1^2 + 24*x1*x2 + 24*x2*x1 + 55*x2^2 ); End. ProgramVariables Real x1; Real x2; Real sint; Real cost; End. Problem x1 = 1/20 & x2 = 1/32 & sint=0 & cost=1 /* t=0 initially */ -> [{ x1'=x2, x2'=-x2-(2+sint)*x1, sint'=cost, cost'=-sint }@invariant(cost^2+sint^2<=100000/99999, cost^2+sint^2>=1)]LyapunovCandidate(x1, x2) < 1 End. Tactic "Scripted proof" implyR(1) ; dC("cost^2+sint^2<=100000/99999", 1) ; <( dC("cost^2+sint^2>=1", 1) ; <( expand("LyapunovCandidate"); dbx(1), dI(1) ), dI(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Flight Maneuvers (I)" Citation "Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell; Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges". Definitions Real w1; End. ProgramVariables Real x; Real y; Real cost; Real sint; End. Problem w1<0 & cost = 1 & sint = 0 & w1^2*(x^2 + y^2) - 8*w1*y > -8*w1 + w1^2 -> [{ x' = 2*cost - 2 + w1*y, y' = 2*sint - w1*x, cost' = 2*w1*sint, sint' = -2*w1*cost } ](x^2 + y^2 > 1) /* Known invariant: w1^2*(x^2 + y^2) + 4*w1*sint*x + 4*w1*(-1 - cost)*y + 8*cost > 8 - 8*w1 + w1^2 */ End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.1" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems;". ProgramVariables Real x1, x2, x3, x4; End. Problem x1 = 1 & x2 = 1 & x3 = 1 & x4 = 1 -> [{x1'=x1 - 2*x2 - x4, x2'=-x1 + 4*x2 - x3 + 2*x4, x3'=2*x2 + x3 + x4, x4'=2*x1 - 4*x2 + 2*x3 - 2*x4}@invariant(x1+x3=x2+x4)]!(x1=10 & x2=0 & x3=2 & x4=3) End. Tactic "Scripted proof" implyR(1) ; dC("x1+x3=x2+x4", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.3 Variant 1" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems; ". ProgramVariables Real x1, x2, x3, x4; End. Problem 0.5*(x1 + x3 + 2*x4)^2 > 3 -> [{x1'=-3*x1+x2+4*x3+2*x4, x2'=8*x1-3*x2-2*x3+6*x4, x3'=-9*x1+3*x2+4*x3-4*x4, x4'=6*x1-3*x2-4*x3+2*x4 }@invariant((-x2 + x4)^2 + (x1 + x3 + 2*x4)^2 > 3) ] ((-x2 + x4)^2 + 2*(x1 + x3 + 2*x4)^2 > 1) End. Tactic "Scripted proof" implyR(1) ; dC("(-x2+x4)^2+(x1+x3+2*x4)^2>3", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Scripted proof (2)" implyR(1) ; dC("x2^2+(x1+x3)^2+2*(2*x1+(-1)*x2+2*x3)*x4+5*x4^2>=50003/8334", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.3 Variant 2" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems; ". ProgramVariables Real x1, x2, x3, x4; End. Problem 3*(x1 - x2 + 2*x4)^2 + 2*(-x1 + 2*x2 + 2*x3)^2 < 1.5 -> [{x1'=-3*x1+x2+4*x3+2*x4, x2'=8*x1-3*x2-2*x3+6*x4, x3'=-9*x1+3*x2+4*x3-4*x4, x4'=6*x1-3*x2-4*x3+2*x4 }@invariant((x1 - x2 + 2*x4)^2 + (-x1 + 2*x2 + 2*x3)^2 < 2) ] !(x2 > 1 & x1 > 4*x2 & x4 > 0) End. Tactic "Scripted proof" implyR(1) ; dC("(x1-x2+2*x4)^2+(-x1+2*x2+2*x3)^2 < 2", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C5" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C5". ProgramVariables Real x, y, z, v; Real u1, u2, u3, u4; End. Problem 1<=x&x<=2 & -0.5<=y&y<=0.5 & -0.5<=z&z<=0.5 & -0.5<=v&v<=0.5 & 0.9<=u1&u1<=1 & 10<=u2&u2<=11 & 1<=u3&u3<=1.2 & -12.5<=u4&u4<=-12 -> [{x'=u1*y, y'=-0.1*y-u2*z+x*v^2, z'=u3*v, v'=u4*x-8*y-11*z-11*v & -2<=x&x<=2 & -2<=y&y<=2 & -2<=z&z<=2 & -2<=v&v<=2} @invariant(1.7232+2.0033*x+0.2440*y+1.9113*z+0.2391*v+0.8790*x^2-0.0610*x*y+0.06351*y^2+0.07210*x*z-0.4338*y*z+0.8232*z^2-0.1248*x*v-0.1016*y*v-0.1525*z*v-0.07057*v^2>=0) ]!(-1.5<=x&x<=-0.5 & -1.5<=y&y<=-0.5 & -1.5<=z&z<=-0.5 & 0.5<=v&v<=1.5) End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C5 (Nonparametric)" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C5". ProgramVariables Real x, y, z, v; Real u1, u2, u3, u4; End. Problem 1<=x&x<=2 & -0.5<=y&y<=0.5 & -0.5<=z&z<=0.5 & -0.5<=v&v<=0.5 & u1=0.95 & u2=10.5 & u3=1.1 & u4=-12.3 -> [{x'=u1*y, y'=-0.1*y-u2*z+x*v^2, z'=u3*v, v'=u4*x-8*y-11*z-11*v & -2<=x&x<=2 & -2<=y&y<=2 & -2<=z&z<=2 & -2<=v&v<=2} @invariant(1.7232+2.0033*x+0.2440*y+1.9113*z+0.2391*v+0.8790*x^2-0.0610*x*y+0.06351*y^2+0.07210*x*z-0.4338*y*z+0.8232*z^2-0.1248*x*v-0.1016*y*v-0.1525*z*v-0.07057*v^2>=0) ]!(-1.5<=x&x<=-0.5 & -1.5<=y&y<=-0.5 & -1.5<=z&z<=-0.5 & 0.5<=v&v<=1.5) End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C6" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C6". ProgramVariables Real x1, x2, x3, x4; Real u1, u2, u3, u4, u5, u6, u7, u8; End. Problem -1.6<=x1&x1<=1.6 & -1.6<=x2&x2<=1.6 & -1.6<=x3&x3<=1.6 & -1.6<=x4&x4<=1.6 & 0.8<=u1&u1<=1 & 0.6<=u2&u2<=0.8 & 1<=u3&u3<=2 & 0.8<=u4&u4<=1.2 & 0.9<=u5&u5<=1.2 & 1<=u6&u6<=2 & 0.8<=u7&u7<=1.05 & 1<=u8&u8<=1.2 -> [{x1'=u1*x2-x3-x4+(u2-x1^2-x2^2-x3^2-x4^2)*x1, x2'=-x1+u3*x3-x4+(u4-x1^2-x2^2-x3^2-x4^2)*x2, x3'=x1-x2+u5*x4+(u6-x1^2-x2^2-x3^2-x4^2)*x3, x4'=x1+u7*x2-x3+(u8-x1^2-x2^2-x3^2-x4^2)*x4 & -2<=x1&x1<=2 & -2<=x2&x2<=2 & -2<=x3&x3<=2 & -2<=x4&x4<=2} @invariant(8.2997-0.18912*x1-0.19551*x2-0.19371*x3-0.18707*x4-0.37075*x1^2 -0.37215*x2^2-0.37283*x3^2-0.37155*x4^2-0.14238*x1*x2-0.14189*x1*x3 -0.14254*x2*x3-0.14137*x1*x4-0.14203*x2*x4-0.14327*x3*x4>=0) ]!(1.8<=x1&x1<=2 & 1.8<=x2&x2<=2 & 1.8<=x3&x3<=2 & 1.8<=x4&x4<=2) End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C6 (Nonparametric)" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C6". ProgramVariables Real x1, x2, x3, x4; Real u1, u2, u3, u4, u5, u6, u7, u8; End. Problem -1.6<=x1&x1<=1.6 & -1.6<=x2&x2<=1.6 & -1.6<=x3&x3<=1.6 & -1.6<=x4&x4<=1.6 & u1=0.9 & u2=0.7 & u3=1.5 & u4=1 & u5=1 & u6=1.5 & u7=1 & u8=1.1 -> [{x1'=u1*x2-x3-x4+(u2-x1^2-x2^2-x3^2-x4^2)*x1, x2'=-x1+u3*x3-x4+(u4-x1^2-x2^2-x3^2-x4^2)*x2, x3'=x1-x2+u5*x4+(u6-x1^2-x2^2-x3^2-x4^2)*x3, x4'=x1+u7*x2-x3+(u8-x1^2-x2^2-x3^2-x4^2)*x4 & -2<=x1&x1<=2 & -2<=x2&x2<=2 & -2<=x3&x3<=2 & -2<=x4&x4<=2} @invariant(8.2997-0.18912*x1-0.19551*x2-0.19371*x3-0.18707*x4-0.37075*x1^2 -0.37215*x2^2-0.37283*x3^2-0.37155*x4^2-0.14238*x1*x2-0.14189*x1*x3 -0.14254*x2*x3-0.14137*x1*x4-0.14203*x2*x4-0.14327*x3*x4>=0) ]!(1.8<=x1&x1<=2 & 1.8<=x2&x2<=2 & 1.8<=x3&x3<=2 & 1.8<=x4&x4<=2) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Papachristodoulou Prajna 2002: Example 3 (Whirling Pendulum)" Citation "Antonis Papachristodoulou, Stephen Prajna. On the Construction of Lyapunov Functions using the Sum of Squares Decomposition. 2002.". Link "https://doi.org/10.1109/CDC.2002.1184414". Definitions Real theta, g, lp; End. ProgramVariables Real x1, x2; Real u1, u2; End. Problem x2 > 0 & x2 < 1 & u1 > 0 & u1 < 1 & u2 > -1/2 & u2 < 1 & theta = 1 & lp = 1 & g = 10 & u1^2+u2^2=1 -> [{x1' = x2, x2' = theta^2*u1*u2 - g/lp*u1, u1' = x2*u2, u2' = -x2*u1 }@invariant(((-20)+u2)*u2+x2^2<=45/4) ]!(u2 < -0.75 & x2 = 4) End. Tactic "Scripted proof" implyR(1) ; dC("((-20)+u2)*u2+x2^2<=45/4", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Lunar lander descent guidance (slow descent low thrust)" Citation "Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, Yao Chen. Formal Verification of a Descent Guidance Control Program of a Lunar Lander; FM 2014.". Definitions import kyx.math.{min,max}; Real Isp1 = 2500; /* thrust engine impulse (low thrust) */ Real Isp2 = 2800; /* thrust engine impulse (high thrust) */ Real gM = 1.622; /* gravitational acceleration on the moon */ Real vslw = -2; /* target velocity slow descent */ Real vmax = 5; /* max velocity */ Real DeltaT = 0.128; /* controller sampling time */ Real mMin = 1100; /* minimum lander mass */ Real mMax = 3000; /* maximum lander mass */ Real c1 = 0.01; /* control coefficient */ Real c2 = 0.6; /* control coefficient */ End. ProgramVariables Real r; /* altitude relative to lunar surface */ Real v; /* vertical velocity */ Real m; /* lunar lander mass */ Real Fc; /* lander thrust */ Real t; /* time */ Real isp; /* engine impulse depending on thrust */ Real a; Real alC; End. Problem m=1250 & r=30 & v=-2 & a = 2027.5/m & alC = max(-c1*(a-gM) - c2*(v-vslw) + gM, 1500/m) & Fc = max(min(m*alC, 5000), 1500) /* <=3000 */ & t=0 & (Fc <= 3000 -> isp=Isp1) & (Fc>3000 -> isp=Isp2) -> [ /* recast per paper */ { r'=v, v'=a-gM, a'=a^2/isp, t'=1 & r>=0 & t<=DeltaT & mMin<=m&m<=mMax } ]v^2<=vmax^2 End. End. ArchiveEntry "Benchmarks/Nonlinear/Lunar lander descent guidance (slow descent high thrust)" Citation "Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, Yao Chen. Formal Verification of a Descent Guidance Control Program of a Lunar Lander; FM 2014.". Definitions import kyx.math.{min,max}; Real Isp1 = 2500; /* thrust engine impulse (low thrust) */ Real Isp2 = 2800; /* thrust engine impulse (high thrust) */ Real gM = 1.622; /* gravitational acceleration on the moon */ Real vslw = -2; /* target velocity slow descent */ Real vmax = 5; /* max velocity */ Real DeltaT = 0.128; /* controller sampling time */ Real mMin = 1100; /* minimum lander mass */ Real mMax = 3000; /* maximum lander mass */ Real c1 = 0.01; /* control coefficient */ Real c2 = 0.6; /* control coefficient */ End. ProgramVariables Real r; /* altitude relative to lunar surface */ Real v; /* vertical velocity */ Real m; /* lunar lander mass */ Real Fc; /* lander thrust */ Real t; /* time */ Real isp; /* engine impulse depending on thrust */ Real a; Real alC; End. Problem m=1250 & r=30 & v=-5 & a = 2027.5/m & alC = max(-c1*(a-gM) - c2*(v-vslw) + gM, 1500/m) & Fc = max(min(m*alC, 5000), 1500) /* >3000 */ & t=0 & (Fc <= 3000 -> isp=Isp1) & (Fc>3000 -> isp=Isp2) -> [ /* recast per paper */ { r'=v, v'=a-gM, a'=a^2/isp, t'=1 & r>=0 & t<=DeltaT & mMin<=m&m<=mMax } ]v^2<=vmax^2 End. End. /* 5D */ ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.13" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems; ". ProgramVariables Real x1, x2, x3, x4, x5; End. Problem x1 > 1 & x3 > x1 & x4 > x3 -> [{x1'=2*(x1-3*x2+2*x3+x5), x2'=2*x1-x2+2*x3+2*x4, x3'=x2-x3, x4'=-3*x1+5*x2-4*x3-x4-2*x5, x5'=4*x2-2*x3+x4 }@invariant(x1 + x3 + x4 > 0, x2^2+4*(x1+x4)*(x1+x3+x4)>0) ] !(x1 < -5 & x3 = -x4) End. Tactic "Automated proof" autoClose End. End. ArchiveEntry "Benchmarks/Nonlinear/Space Craft: Collision Avoidance" Citation "Fabian Immler, Matthias Althoff, Xin Chen, Chuchu Fan, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Mahendra Singh Tomar, and Majid Zamani. ARCH-COMP18 Category Report: Continuous and Hybrid Systems with nonlinear Dynamics". Definitions Real n; Real mu = 3.986*10^14*60^2; Real r = 42164*10^3; Real irc; Real mc = 500; End. ProgramVariables Real x; Real y; Real vx; Real vy; Real t; Real ux; Real uy; End. Problem n^2 = mu/r^3 & 1 = irc^2 * ((r+x)^2 + y^2) & -925 <= x & x <= -875 & -425 <= y & y <= -375 & vx = 0 & vy = 0 & t = 0 -> [{ x'=vx, y'=vy, vx'=n^2*x+2*n*vy+mu/r^2-mu*irc^3*(r+x)+ux/mc, vy'=n^2*y-2*n*vx-mu*irc^3*y+uy/mc, t'=1 & t<=200 } ]( x^2 > 0.2^2 | y^2 > 0.2^2 ) End. End. /* 6D */ ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C7" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C7". ProgramVariables Real x1, x2, x3, x4, x5, x6; Real u1, u2, u3, u4, u5, u6; End. Problem (x1-3.05)^2+(x2-3.05)^2+(x3-3.05)^2+(x4-3.05)^2+(x5-3.05)^2+(x6-3.05)^2<=0.05^2 & 0.9<=u1&u1<=1 & 0.9<=u2&u2<=1 & 1<=u3&u3<=1.1 & 1<=u4&u4<=1.1 & 0.9<=u5&u5<=1 & 1<=u6&u6<=1.1 -> [{x1'=-u1*x1^3+4*x2^3-6*x3*x4, x2'=-x1-u2*x2+x5^3, x3'=x1*x4-u3*x3+x4*x6, x4'=x1*x3+x3*x6-u4*x4^3, x5'=-2*x2^3-u5*x5+x6, x6'=-3*x3*x4-x5^3-u6*x6 & 0<=x1&x1<=10 & 0<=x2&x2<=10 & 2<=x3&x3<=10 & 0<=x4&x4<=10 & 0<=x5&x5<=10 & 0<=x6&x6<=10} @invariant(-0.1182-0.06094*x1-0.00726*x2+0.3824*x3+0.3248*x4-0.1632*x5-0.1656*x6 +0.03366*x1*x2-0.006225*x1*x3-0.004584*x1*x4-0.009548*x1*x5+0.01588*x1*x6 -0.003326*x2*x3+0.005185*x2*x4+0.01407*x2*x5-0.01693*x2*x6+0.04518*x3*x4 -0.0167*x3*x5-0.008248*x3*x6+0.004361*x4*x5+0.01167*x4*x6+0.0214*x5*x6 -0.009488*x1^2-0.009429*x2^2-0.06402*x3^2-0.08304*x4^2+0.005361*x5^2-0.007063*x6^2>=0) ]!((x1-4.05)^2+(x2-4.15)^2+(x3-4.25)^2+(x4-4.35)^2+(x5-4.45)^2+(x6-4.55)^2<=0.05^2) End. End. ArchiveEntry "Benchmarks/Nonlinear/Yang Wu Lin 2020: Benchmark C7 (Nonparametric)" Citation "Z. Yang, M. Wu and W. Lin, nonlinear Analysis: Hybrid Systems (36), 2020, Benchmark C7". ProgramVariables Real x1, x2, x3, x4, x5, x6; Real u1, u2, u3, u4, u5, u6; End. Problem (x1-3.05)^2+(x2-3.05)^2+(x3-3.05)^2+(x4-3.05)^2+(x5-3.05)^2+(x6-3.05)^2<=0.05^2 & u1=0.95 & u2=0.95 & u3=1.05 & u4=1.05 & u5=0.95 & u6=1.05 -> [{x1'=-u1*x1^3+4*x2^3-6*x3*x4, x2'=-x1-u2*x2+x5^3, x3'=x1*x4-u3*x3+x4*x6, x4'=x1*x3+x3*x6-u4*x4^3, x5'=-2*x2^3-u5*x5+x6, x6'=-3*x3*x4-x5^3-u6*x6 & 0<=x1&x1<=10 & 0<=x2&x2<=10 & 2<=x3&x3<=10 & 0<=x4&x4<=10 & 0<=x5&x5<=10 & 0<=x6&x6<=10} @invariant(-0.1182-0.06094*x1-0.00726*x2+0.3824*x3+0.3248*x4-0.1632*x5-0.1656*x6 +0.03366*x1*x2-0.006225*x1*x3-0.004584*x1*x4-0.009548*x1*x5+0.01588*x1*x6 -0.003326*x2*x3+0.005185*x2*x4+0.01407*x2*x5-0.01693*x2*x6+0.04518*x3*x4 -0.0167*x3*x5-0.008248*x3*x6+0.004361*x4*x5+0.01167*x4*x6+0.0214*x5*x6 -0.009488*x1^2-0.009429*x2^2-0.06402*x3^2-0.08304*x4^2+0.005361*x5^2-0.007063*x6^2>=0) ]!((x1-4.05)^2+(x2-4.15)^2+(x3-4.25)^2+(x4-4.35)^2+(x5-4.45)^2+(x6-4.55)^2<=0.05^2) End. End. ArchiveEntry "Benchmarks/Nonlinear/Gorbuzov Pranevich 2012: Example 1.6" Citation "V.N. Gorbuzov, A.F. Pranevich: First integrals of ordinary linear differential systems;". ProgramVariables Real x1, x2, x3, x4, x5, x6; End. Problem x5 > -5 & x5 < x1 & x2 > x1 + 8 & x1 >= -1 -> [{x1'=x1-2*x2+x3-2*x6, x2'=3*x2-x3-x5+2*x6, x3'=-x1+x3+2*x4+2*x5, x4'=-x1+x4+x5+x6, x5'=x1+x2+x5, x6'=x1-x2+x3-x4-x6 & x5 < 0 }@invariant(x1+x2+x5 >= 0) ]!(x2 < 0 & x1 < x2 & x5 < x2) End. Tactic "Scripted proof" implyR(1) ; dC("x1+x2+x5>=0", 1) ; <( dW(1) ; QE, dbx(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Djaballah Chapoutot Kieffer Bouissou 2017: Example 8" Description "Example 8, p; 293". Citation "Adel Djaballah, Alexandre Chapoutot, Michel Kieffer, Olivier Bouissou; Construction of parametric barrier functions for dynamical systems using interval analysis; Automatica 78 (2017) 287–296. From Antonis Papachristodoulou, Stephen Prajna. On the Construction of Lyapunov Functions using the Sum of Squares Decomposition. 2002. (Example 1)". Link "https://doi.org/10.1016/j.automatica.2016.12.013". ProgramVariables Real x1, x2, x3, x4, x5, x6; End. Problem (x1-3.05)^2 + (x2-3.05)^2 + (x3-3.05)^2 + (x4-3.05)^2 + (x5-3.05)^2 + (x6-3.05)^2 - 0.0001 <= 0 -> [{x1' = -x1^3 + 4*x2^3 - 6*x3*x4, x2' = -x1 - x2 + x5^3, x3' = x1*x4 - x3 + x4*x6, x4' = x1*x3 + x3*x6 - x4^3, x5' = -2*x2^3 - x5 + x6, x6' = -3*x3*x4 - x5^3 - x6 & 0<=x1 & x1<=10 & 0<=x2 & x2<=10 & 2<=x3 & x3<=10 & 0<=x4 & x4<=10 & 0<=x5 & x5<=10 & 0<=x6 & x6<=10 } ]!((x1-7.05)^2 + (x2-3.05)^2 + (x3-7.05)^2 + (x4-7.05)^2 + (x5-7.05)^2 + (x6-7.05)^2 - 0.0001 <= 0) End. End. /* 7 D */ ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C9" Description "Example C9". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; Real x3; Real x4; Real x5; Real x6; Real x7; End. Problem 0.99 <= x1 & x1 <= 1.01 & 0.99 <= x2 & x2 <= 1.01 & 0.99 <= x3 & x3 <= 1.01 & 0.99 <= x4 & x4 <= 1.01 & 0.99 <= x5 & x5 <= 1.01 & 0.99 <= x6 & x6 <= 1.01 & 0.99 <= x7 & x7 <= 1.01 -> [ { x1' = -0.4*x1 + 5*x3*x4, x2' = 0.4*x1 - x2, x3' = x2 - 5*x3*x4, x4' = 5*x5*x6 - 5*x3*x4, x5' = -5*x5*x6 + 5*x3*x4, x6' = 0.5*x7 - 5*x5*x6, x7' = -0.5*x7 + 5*x5*x6 & -2 <= x1 & x1 <= 2 & -2 <= x2 & x2 <= 2 & -2 <= x3 & x3 <= 2 & -2 <= x4 & x4 <= 2 & -2 <= x5 & x5 <= 2 & -2 <= x6 & x6 <= 2 & -2 <= x7 & x7 <= 2 }@invariant(x1+x2+x3<=706/233) ] !( 1.8 <= x1 & x1 <= 2 & 1.8 <= x2 & x2 <= 2 & 1.8 <= x3 & x3 <= 2 & 1.8 <= x4 & x4 <= 2 & 1.8 <= x5 & x5 <= 2 & 1.8 <= x6 & x6 <= 2 & 1.8 <= x7 & x7 <= 2 ) End. Tactic "Scripted proof" implyR(1) ; dC("x1+x2+x3<=706/233", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. /* 8 D */ ArchiveEntry "Benchmarks/Nonlinear/Collision Avoidance Maneuver (I)" Citation "Sriram Sankaranarayanan. Automatic Invariant Generation for Hybrid Systems Using Ideal Fixed Points". Definitions Real a; Real b; Real r1; Real r2; Real w; Real theta; End. ProgramVariables Real x1; Real x2; Real d1; Real d2; Real y1; Real y2; Real e1; Real e2; End. Problem x1=r1 & y1=r1 & x2=r2 & y2=r2 & d1=a & d2=0 /* seems like there is a typo in the paper, e1,e2 should be flipped */ & e1=0 & e2=b -> [ {x1'=d1, x2'=d2, d1'=-w*d2, d2'=w*d1, y1'=e1, y2'=e2, e1'=-theta*e2, e2'=theta*e1} @invariant(e1^2+e2^2-b()^2=0, d1^2+d2^2-a()^2=0, e1-r2()*theta()+theta()*y2=0, -a()+d1-r2()*w()+w()*x2=0) ] (e1 - r2*theta + theta * y2) != e2^2 + 1 /* Invariants from paper: e1^2 + e2^2 - b^2 = 0 d1^2 + d2^2 - a^2 = 0 e1 - r2*theta + theta * y2 = 0 -a + d1 - r2*w + w*x2 = 0 b - e2 - r1*theta + theta*y1 = 0 -b*r1 + b*y1 + e1*r2 - e1*y2 - e2*r1 + e2*y1 = 0 b*r2 - b*y2 - e1*r1 + e1*y1 - e2*r2 + e2*y2 = 0 -d2 - r1*w + w*x1 = 0 a*d2*r2 - a*d2*x2 + d1*d2*r2 - d1*d2*x2 - r1*d2^2*r1 + d2^2*x1 = 0 a*r1 - a*x1 - d1*r1 + d1*x1 - d2*r2 + d2*x2 = 0 */ End. Tactic "Scripted proof" implyR(1) ; dC("e1^2+e2^2-b()^2=0", 1) ; <( dC("d1^2+d2^2-a()^2=0", 1) ; <( dC("e1-r2()*theta()+theta()*y2=0", 1) ; <( dC("-a()+d1-r2()*w()+w()*x2=0", 1) ; <( dW(1) ; QE, dI(1) ), dI(1) ), dI(1) ), dI(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/ATC: 2 Aircraft Tangential Roundabout Maneuver (ODE)" Description "Essentials of Tangential Roundabout Maneuver (TRM) in Air Traffic Control (ATC)". Citation "Andre Platzer. Differential-algebraic dynamic logic for differential-algebraic programs; Journal of Logic and Computation, 20(1), pages 309-352, 2010.". Link "https://doi.org/10.1093/logcom/exn070". Definitions Real p; /* protected zone radius */ Real om; /* angular velocity of aircraft 1 */ Real omy; /* angular velocity of aircraft 2 */ Real c1; /* x-position of center of roundabout circle */ Real c2; /* y-position of center of roundabout circle */ Bool safeSeparation(Real x1, Real y1, Real x2, Real y2) <-> ( (x1-y1)^2 + (x2-y2)^2 >= p^2 ); End. ProgramVariables Real x1; /* x-position of aircraft 1 */ Real x2; /* y-position of aircraft 1 */ Real d1; /* x-direction of aircraft 1 */ Real d2; /* y-direction of aircraft 1 */ Real y1; /* x-position of aircraft 2 */ Real y2; /* y-position of aircraft 2 */ Real e1; /* x-direction of aircraft 2 */ Real e2; /* y-direction of aircraft 2 */ End. Problem safeSeparation(x1, y1, x2, y2) & d1 =-om*(x2-c2) & d2=om*(x1-c1) & e1 =-om*(y2-c2) & e2=om*(y1-c1) -> [{x1'=d1, x2'=d2, d1'=-om*d2, d2'=om*d1, y1'=e1, y2'=e2, e1'=-om*e2, e2'=om*e1}@invariant(d1-e1=-om()*(x2-y2)&d2-e2=om()*(x1-y1)) ]safeSeparation(x1, y1, x2, y2) End. Tactic "Scripted proof" implyR(1) ; dC("d1-e1=-om()*(x2-y2)&d2-e2=om()*(x1-y1)", 1) ; <( dI(1), dI(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Collision Avoidance Maneuver (II)" Citation "Jiang Liu, Naijun Zhan, Hengjun Zhao. Computing Semi-algebraic Invariants for Polynomial Dynamical Systems". Definitions Real w1; Real w2; Real xi1; Real xi2; Real di1; Real di2; Real yi1; Real yi2; Real ei1; Real ei2; End. ProgramVariables Real x1; Real x2; Real d1; Real d2; Real y1; Real y2; Real e1; Real e2; End. Problem x1 = xi1 & x2 = xi2 & d1 = di1 & d2 = di2 & y1 = yi1 & y2 = yi2 & e1 = ei1 & e2 = ei2 -> [ {x1'=d1, x2'=d2, d1'=-w1*d2, d2'=w1*d1, y1'=e1, y2'=e2, e1'=-w2*e2, e2'=w2*e1} @invariant(w1*x2 + d1 - w1*xi2 - di1 = 0, -w1*x1 + d2 + w1*xi1 - di2 = 0, -w1*x1 + w1*x2 + d1 + d2 + w1*xi1 - w1*xi2 - di1 - di2 = 0, d1^2 + d2^2 - di1^2 - di2^2 = 0) ] -w1*x1 + 3*w1*x2 + 3*d1 + d2 + w1*xi1 - 3*w1*xi2 - 3*di1 - di2 >= -d1^2 End. Tactic "Scripted proof" implyR(1) ; dC("w1()*x2+d1-w1()*xi2()-di1()=0", 1) ; <( dC("-w1()*x1+d2+w1()*xi1()-di2()=0", 1) ; <( dC("-w1()*x1+w1()*x2+d1+d2+w1()*xi1()-w1()*xi2()-di1()-di2()=0", 1) ; <( dC("d1^2+d2^2-di1()^2-di2()^2=0", 1) ; <( dW(1) ; QE, dI(1) ), dI(1) ), dI(1) ), dI(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Collision Avoidance Maneuver (III)" Citation "Khalil Ghorbal and André Platzer. Characterizing algebraic invariants by differential radical invariants. In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Proceedings, volume 8413 of LNCS, pp; 279-294. Springer, 2014.". Definitions Real w1; Real w2; End. ProgramVariables Real x1; Real x2; Real d1; Real d2; Real y1; Real y2; Real e1; Real e2; End. Problem w1=w2 & d1=2 & d2=4 & e1=-2 & e2=-4 -> [{ x1'=d1, x2'=d2, d1'=-w1*d2, d2'=w1*d1, y1'=e1, y2'=e2, e1'=-w2*e2, e2'=w2*e1 } ] ((d1+d2+e1+e2)^2 < 1 & (d1-d2+e1-e2)*(d1+d2+e1+e2) > -1) /* Invariant (family) from paper: g1*d1 + g2*d2 + g3*e1 + g4*e2 = 0 & g2*d1 - g1*d2 + g4*e1 - g3*e2 = 0 */ End. End. ArchiveEntry "Benchmarks/Nonlinear/Laub-Loomis" Citation "Fabian Immler, Matthias Althoff, Xin Chen, Chuchu Fan, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Mahendra Singh Tomar, and Majid Zamani. ARCH-COMP18 Category Report: Continuous and Hybrid Systems with nonlinear Dynamics". Definitions Real W; Bool in(Real v, Real c, Real w) <-> ( c-w <= v & v <= c+w ); End. ProgramVariables Real x1; Real x2; Real x3; Real x4; Real x5; Real x6; Real x7; Real t; End. Problem W=0.1 & in(x1,1.2,W) & in(x2,1.05,W) & in(x3,1.5,W) & in(x4,2.4,W) & in(x5,1,W) & in(x6,0.1,W) & in(x7,0.45,W) & t=0 -> [{ x1'=1.4*x3-0.9*x1, x2'=2.5*x5-1.5*x2, x3'=0.6*x7-0.8*x2*x3, x4'=2-1.3*x3*x4, x5'=0.7*x1-x4*x5, x6'=0.3*x1-3.1*x6, x7'=1.8*x6-1.5*x2*x7, t'=1 & t<=20 }](x4 < 5) End. End. /* 9 D */ ArchiveEntry "Benchmarks/Nonlinear/Planar 2-body problem" Definitions Real m; End. ProgramVariables Real x1; Real y1; Real vx1; Real vy1; Real x2; Real y2; Real vx2; Real vy2; Real r; End. Problem r = 1 & x1 = 0 & y1 = 0 & vx1 = 0 & vy1 = -1 & x2 = 1 & y2 = 0 & vx2 = 0 & vy2 = 1 & m = 5 -> [{ r' = -r^3*((x1 - x2)*(vx1 - vx2) + (y1 - y2)*(vy1 - vy2)), x1' = vx1, vx1' = -m*(x1 - x2)*r^3, y1' = vy1, vy1' = -m*(y1 - y2)*r^3, x2' = vx2, vx2' = -m*(x2 - x1)*r^3, y2' = vy2, vy2' = -m*(y2 - y1)*r^3 }] (x1-x2)^2+(y1-y2)^2 <= 2 End. End. ArchiveEntry "Benchmarks/Nonlinear/ZYLZCL Example C10" Description "Example C10". Citation "Yifan Zhang, Zhengfeng Yang, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li. Safety Verification of nonlinear Hybrid Systems Based on Bilinear Programming;". ProgramVariables Real x1; Real x2; Real x3; Real x4; Real x5; Real x6; Real x7; Real x8; Real x9; End. Problem 0.99 <= x1 & x1 <= 1.01 & 0.99 <= x2 & x2 <= 1.01 & 0.99 <= x3 & x3 <= 1.01 & 0.99 <= x4 & x4 <= 1.01 & 0.99 <= x5 & x5 <= 1.01 & 0.99 <= x6 & x6 <= 1.01 & 0.99 <= x6 & x6 <= 1.01 & 0.99 <= x7 & x7 <= 1.01 & 0.99 <= x8 & x8 <= 1.01 & 0.99 <= x9 & x9 <= 1.01 -> [ { x1' = 3*x3 - x1*x6, x2' = x4 - x2*x6, x3' = x1*x6 - 3*x3, x4' = x2*x6 - x4, x5' = 3*x3 + 5*x1 - x5, x6' = 5*x5 + 3*x3 + x4 - x6*(x1 + x2 + 2*x8 + 1), x7' = 5*x4 + x2 - 0.5*x7, x8' = 5*x7 - 2*x6*x8 + x9 - 0.2*x8, x9' = 2*x6*x8 - x9 & -2 <= x1 & x1 <= 2 & -2 <= x2 & x2 <= 2 & -2 <= x3 & x3 <= 2 & -2 <= x4 & x4 <= 2 & -2 <= x5 & x5 <= 2 & -2 <= x6 & x6 <= 2 & -2 <= x7 & x7 <= 2 & -2 <= x8 & x8 <= 2 & -2 <= x9 & x9 <= 2 }@invariant(x2+x4<=101/50) ] !( 1.8 <= x1 & x1 <= 2 & 1.8 <= x2 & x2 <= 2 & 1.8 <= x3 & x3 <= 2 & 1.8 <= x4 & x4 <= 2 & 1.8 <= x5 & x5 <= 2 & 1.8 <= x6 & x6 <= 2 & 1.8 <= x7 & x7 <= 2 & 1.8 <= x8 & x8 <= 2 & 1.8 <= x9 & x9 <= 2 ) End. Tactic "Scripted proof" implyR(1) ; dC("x2+x4<=101/50", 1) ; <( dW(1) ; QE, dI(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. /* 12D */ ArchiveEntry "Benchmarks/Nonlinear/ATC: 3 Aircraft Tangential Roundabout Maneuver (ODE)" Description "Essentials of Tangential Roundabout Maneuver (TRM) in Air Traffic Control (ATC)". Citation "Andre Platzer. Differential-algebraic dynamic logic for differential-algebraic programs; Journal of Logic and Computation, 20(1), pages 309-352, 2010.". Link "https://doi.org/10.1093/logcom/exn070". Definitions Real p; /* protected zone radius */ Real om; /* angular velocity of aircraft 1 */ Real omy; /* angular velocity of aircraft 2 */ Real omz; /* angular velocity of aircraft 3 */ Real c1; /* x-position of center of roundabout circle */ Real c2; /* y-position of center of roundabout circle */ Bool safeSeparation(Real x1, Real y1, Real x2, Real y2) <-> ( (x1-y1)^2 + (x2-y2)^2 >= p^2 ); Bool safeSeparation3(Real x1, Real y1, Real x2, Real y2, Real z1, Real z2) <-> safeSeparation(x1, y1, x2, y2) & safeSeparation(y1, z1, y2, z2) & safeSeparation(x1, z1, x2, z2); End. ProgramVariables Real x1; /* x-position of aircraft 1 */ Real x2; /* y-position of aircraft 1 */ Real d1; /* x-direction of aircraft 1 */ Real d2; /* y-direction of aircraft 1 */ Real y1; /* x-position of aircraft 2 */ Real y2; /* y-position of aircraft 2 */ Real e1; /* x-direction of aircraft 2 */ Real e2; /* y-direction of aircraft 2 */ Real z1; /* x-position of aircraft 3 */ Real z2; /* y-position of aircraft 3 */ Real f1; /* x-direction of aircraft 3 */ Real f2; /* y-direction of aircraft 3 */ End. Problem safeSeparation3(x1, y1, x2, y2, z1, z2) & d1=-om*(x2-c2) & d2=om*(x1-c1) & e1=-om*(y2-c2) & e2=om*(y1-c1) & f1=-om*(z2-c2) & f2=om*(z1-c1) -> [ {x1'=d1, x2'=d2, d1'=-om*d2, d2'=om*d1, y1'=e1, y2'=e2, e1'=-om*e2, e2'=om*e1, z1'=f1, z2'=f2, f1'=-om*f2, f2'=om*f1}@invariant(d1=-om()*(x2-c2())&d2=om()*(x1-c1())&e1=-om()*(y2-c2())&e2=om()*(y1-c1())&f1=-om()*(z2-c2())&f2=om()*(z1-c1())) ]safeSeparation3(x1, y1, x2, y2, z1, z2) End. Tactic "Scripted proof" implyR(1) ; dC("d1=-om()*(x2-c2())&d2=om()*(x1-c1())&e1=-om()*(y2-c2())&e2=om()*(y1-c1())&f1=-om()*(z2-c2())&f2=om()*(z1-c1())", 1) ; <( dI(1), dI(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. /* 16D */ ArchiveEntry "Benchmarks/Nonlinear/ATC: 4 Aircraft Tangential Roundabout Maneuver (ODE)" Description "Essentials of Tangential Roundabout Maneuver (TRM) in Air Traffic Control (ATC)". Citation "Andre Platzer. Differential-algebraic dynamic logic for differential-algebraic programs; Journal of Logic and Computation, 20(1), pages 309-352, 2010.". Link "https://doi.org/10.1093/logcom/exn070". Definitions Real p; /* protected zone radius */ Real om; /* angular velocity of aircraft 1 */ Real omy; /* angular velocity of aircraft 2 */ Real omz; /* angular velocity of aircraft 3 */ Real omu; /* angular velocity of aircraft 4 */ Real c1; /* x-position of center of roundabout circle */ Real c2; /* y-position of center of roundabout circle */ Bool safeSeparation(Real x1, Real y1, Real x2, Real y2) <-> ( (x1-y1)^2 + (x2-y2)^2 >= p^2 ); Bool safeSeparation4(Real x1, Real y1, Real x2, Real y2, Real z1, Real z2, Real u1, Real u2) <-> safeSeparation(x1, y1, x2, y2) & safeSeparation(y1, z1, y2, z2) & safeSeparation(x1, z1, x2, z2) & safeSeparation(x1, u1, x2, u2) & safeSeparation(y1, u1, y2, u2) & safeSeparation(z1, u1, z2, u2); End. ProgramVariables Real x1; /* x-position of aircraft 1 */ Real x2; /* y-position of aircraft 1 */ Real d1; /* x-direction of aircraft 1 */ Real d2; /* y-direction of aircraft 1 */ Real y1; /* x-position of aircraft 2 */ Real y2; /* y-position of aircraft 2 */ Real e1; /* x-direction of aircraft 2 */ Real e2; /* y-direction of aircraft 2 */ Real z1; /* x-position of aircraft 3 */ Real z2; /* y-position of aircraft 3 */ Real f1; /* x-direction of aircraft 3 */ Real f2; /* y-direction of aircraft 3 */ Real u1; /* x-position of aircraft 4 */ Real u2; /* y-position of aircraft 4 */ Real g1; /* x-direction of aircraft 4 */ Real g2; /* y-direction of aircraft 4 */ End. Problem safeSeparation4(x1, y1, x2, y2, z1, z2, u1, u2) & d1=-om*(x2-c2) & d2=om*(x1-c1) & e1=-om*(y2-c2) & e2=om*(y1-c1) & f1=-om*(z2-c2) & f2=om*(z1-c1) & g1=-om*(u2-c2) & g2=om*(u1-c1) -> [ {x1'=d1, x2'=d2, d1'=-om*d2, d2'=om*d1, y1'=e1, y2'=e2, e1'=-om*e2, e2'=om*e1, z1'=f1, z2'=f2, f1'=-om*f2, f2'=om*f1, u1'=g1, u2'=g2, g1'=-om*g2, g2'=om*g1}@invariant((d1=-om()*(x2-c2())&d2=om()*(x1-c1()))&(e1=-om()*(y2-c2())&e2=om()*(y1-c1()))&(f1=-om()*(z2-c2())&f2=om()*(z1-c1()))&g1=-om()*(u2-c2())&g2=om()*(u1-c1())) ]safeSeparation4(x1, y1, x2, y2, z1, z2, u1, u2) End. Tactic "Scripted proof" implyR(1) ; dC("(d1=-om()*(x2-c2())&d2=om()*(x1-c1()))&(e1=-om()*(y2-c2())&e2=om()*(y1-c1()))&(f1=-om()*(z2-c2())&f2=om()*(z1-c1()))&g1=-om()*(u2-c2())&g2=om()*(u1-c1())", 1) ; <( dI(1), dI(1) ) End. Tactic "Automated proof (from annotations)" auto End. End. /* Product System Problems */ /* 4 D */ ArchiveEntry "Benchmarks/Nonlinear/Product of Arrowsmith Place Fig_3_5e page 79 and Dumortier Llibre Artes Ex. 10_9" ProgramVariables Real yleft; Real xleft; Real xright; Real yright; End. Problem (xleft=1&yleft=-1)&(-1+xright)^2+(1+yright)^2 < 1/4->[{xleft'=xleft^2+(xleft+yleft)/2,yleft'=(-xleft+3*yleft)/2,xright'=xright^4+2*xright*yright^2-6*xright^2*yright^2+yright^4+xright*(xright^2-yright^2),yright'=2*xright^2*yright-4*xright^3*yright+4*xright*yright^3-yright*(xright^2-yright^2)&true&true}](!yleft>0&!yright>=1) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Ben Sassi Girard Sankaranarayanan 2014 Fitzhugh-Nagumo and Strogatz Example 6_8_3" ProgramVariables Real yleft; Real xleft; Real xright; Real yright; End. Problem -1/20+(5/4+xleft)^2+(-5/4+yleft)^2<=0&2*(-1/3+xright)^2+yright^2 < 1/16->[{xleft'=7/8+xleft-xleft^3/3-yleft,yleft'=2*(7/10+xleft-4*yleft/5)/25,xright'=xright^2*yright,yright'=xright^2-yright^2&true&true}](!36/5+5*xleft+xleft^2+2*yleft+yleft^2<=0&!xright<=-2) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Dai Gan Xia Zhan JSC14 Ex. 2 and Fitzhugh Nagumo Ben Sassi Girard 2" ProgramVariables Real yleft; Real aright; Real xleft; Real yright; End. Problem xleft^2+(2+yleft)^2<=1&-1<=aright&aright<=-0.5&1<=yright&yright<=1.5->[{xleft'=2*xleft-xleft*yleft,yleft'=2*xleft^2-yleft,aright'=7/8+aright-aright^3/3-yright,yright'=2*(7/10+aright-4*yright/5)/25&true&true}](!xleft^2+(-1+yleft)^2<=9/100&!(-2.5<=aright&aright<=-2&-2<=yright&yright<=-1.5)) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Dai Gan Xia Zhan JSC14 Ex. 2 and Strogatz Exercise 6_6_1 Reversible System" ProgramVariables Real yleft; Real xleft; Real xright; Real yright; End. Problem xleft^2+(2+yleft)^2<=1&(-1/3+xright)^2+(-1/3+yright)^2 < 1/16->[{xleft'=2*xleft-xleft*yleft,yleft'=2*xleft^2-yleft,xright'=(1-xright^2)*yright,yright'=1-yright^2&true&true}](!xleft^2+(-1+yleft)^2<=9/100&!(xright>=2|xright<=-2)) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Dumortier Llibre Artes Ex. 1_11a and ZYLZCL Example C4" ProgramVariables Real yleft; Real xleft; Real x1right; Real x2right; End. Problem (xleft>-1/2&xleft < -1/3&yleft < 0&yleft>=-1/2)&-1<=x1right&x1right<=0&-1<=x2right&x2right<=0 -> [{xleft'=2*xleft-xleft^5-xleft*yleft^4,yleft'=yleft-xleft^2*yleft-yleft^3, x1right'=-1+x1right^2+x2right^2,x2right'=5*(-1+x1right*x2right)&true&-2<=x1right&x1right<=2&-2<=x2right&x2right<=2 }@invariant(xleft < 0, yleft < 0, 22667*x1right^2+x2right*(257910+6221*x2right)+x1right*(141840+15973*x2right) < 42786) ](!xleft+yleft>0&!(1<=x1right&x1right<=2&1<=x2right&x2right<=2)) End. Tactic "Automated proof" autoClose End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Forsman Phd Ex 6_1 page 99 and ZYLZCL Example C7" ProgramVariables Real yleft; Real xleft; Real x1right; Real x2right; End. Problem xleft^2+(-2+yleft)^2 < 1/24&-3/2<=x1right&x1right<=-1/2&-3/2<=x2right&x2right<=-1/2 -> [{xleft'=-xleft+2*xleft^2*yleft,yleft'=-yleft,x1right'=-x1right+x1right*x2right, x2right'=-x2right&true&-2<=x1right&x1right<=2&-2<=x2right&x2right<=2 }@invariant(x2right+yleft>0, x2right^2+x2right*yleft+yleft^2>0, x1right < 0, x2right < 0, xleft*yleft < 1) ](!(xleft<=-2|yleft<=-1)&!(-1/2<=x1right&x1right<=1/2&1/2<=x2right&x2right<=3/2)) End. Tactic "Scripted proof" implyR(1) ; dC("x2right+yleft>0", 1) ; <( dC("x2right^2+x2right*yleft+yleft^2>0", 1) ; <( dC("x1right < 0", 1) ; <( dC("x2right < 0", 1) ; <( dC("xleft*yleft < 1", 1) ; <( ODEinv(1), dbx(1) ), dbx(1) ), dbx(1) ), dbx(1) ), dbx(1) ) End. Tactic "Automated proof" auto End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Hamiltonian System 1 and Nonlinear Circuit Example 4" ProgramVariables Real yleft; Real xleft; Real x1right; Real x2right; End. Problem (2/3+xleft)^2+yleft^2<=1/24&-1.1<=x1right&x1right<=-0.7&0.5<=x2right&x2right<=0.9 -> [{xleft'=-2*yleft,yleft'=-2*xleft-3*xleft^2,x1right'=-x2right^3,x2right'=x1right-x1right^3&true&true} @invariant(x2right+yleft>0, x2right^2+x2right*yleft+yleft^2>0, x1right < 0, x2right < 0, xleft*yleft < 1) ](!xleft>0&x1right^2+x2right-3 < 0) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Man Maccallum Goriely Page 57 and ZYLZCL Example C1" ProgramVariables Real yleft; Real xleft; Real x1right; Real x2right; End. Problem xleft^2+yleft^2<=1/4&4<=x1right&x1right<=4.5&1<=x2right&x2right<=2 -> [{xleft'=-yleft+2*xleft^2*yleft,yleft'=yleft+2*xleft*yleft^2,x1right'=-11/2*x2right+x2right^2,x2right'=6*x1right-x1right^2&true&1<=x1right&x1right<=5&1<=x2right&x2right<=5} @invariant(349+4*((-9)+x1right)*x1right^2+x2right^2*((-33)+4*x2right)<=0, 2*xleft^2 < 1) ](!xleft>3&!(1<=x1right&x1right<=2&2<=x2right&x2right<=3)) End. Tactic "Scripted proof" implyR(1) ; dC("349+4*((-9)+x1right)*x1right^2+x2right^2*((-33)+4*x2right)<=0", 1) ; <( dC("2*xleft^2 < 1", 1) ; <( dW(1) ; QE, dbx(1) ), dI(1) ) End. Tactic "Automated proof" auto End. End. /* 5 D */ ArchiveEntry "Benchmarks/Nonlinear/Product of Arrowsmith Place Fig_3_5e page 79 and 3D Lotka Volterra (I)" ProgramVariables Real yleft; Real xleft; Real xright; Real yright; Real zright; End. Problem (xleft=1&yleft=-1)&xright=1&yright=1&zright=1->[{xleft'=xleft^2+(xleft+yleft)/2,yleft'=(-xleft+3*yleft)/2,xright'=xright*yright-xright*zright,yright'=yright*zright-yright*xright,zright'=zright*xright-zright*yright&true&true}](!yleft>0&xright+2*yright+zright^3>0) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Darboux Christoffel Int Goriely page 58 and Invariant Clusters Example 5" ProgramVariables Real yleft; Real xleft; Real xright; Real yright; Real zright; End. Problem xleft^2+yleft^2<=1&xright=1&yright=2&zright=3->[{xleft'=3*(-4+xleft^2),yleft'=3+xleft*yleft-yleft^2,xright'=yright*zright,yright'=xright*zright,zright'=xright*yright&true&true}](!(xleft < -4|yleft < -4|xleft>4|yleft>4)&!(xright=5&yright^2=27&zright^2=34)) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Djaballah Chapoutot Kieffer Bouissou 2015 Ex. 1 and Invariant Clusters Example 4" ProgramVariables Real yleft; Real xleft; Real xright; Real yright; Real zright; End. Problem -1/20+(5/4+xleft)^2+(-5/4+yleft)^2<=0&xright=1&yright=2&zright=3->[{xleft'=xleft+yleft,yleft'=xleft*yleft-yleft^2/2,xright'=yright*zright,yright'=xright*zright,zright'=xright*yright&true&true}](!(5/2+xleft)^2+(-4/5+yleft)^2<=1/20&!(xright=5&yright^2=27&zright^2=34)) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Forsman Phd Ex 6_14 page 119 and ZYLZCL Example C2" ProgramVariables Real x3right; Real yleft; Real xleft; Real x1right; Real x2right; End. Problem xleft^2+(-1+yleft)^2 < 1/8&-0.25<=x1right&x1right<=0.75&-0.25<=x2right&x2right<=0.75&-0.75<=x3right&x3right<=0.25->[{xleft'=-2*xleft+yleft^4,yleft'=-yleft+3*xleft*yleft^3,x1right'=-x2right,x2right'=-x3right,x3right'=-x1right-2*x2right-x3right+x1right^3&true&-2<=x1right&x1right<=2&-2<=x2right&x2right<=2&-2<=x3right&x3right<=2}](!yleft<=-1&!(1<=x1right&x1right<=2&-2<=x2right&x2right<=-1&-2<=x3right&x3right<=-1)) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Locally stable nonlinear system and Invariant 3-dim sphere" ProgramVariables Real yleft; Real xleft; Real xright; Real yright; Real zright; End. Problem (xleft^2<=1/2&(yleft+2)^2<=1/3)&xright=1/4&yright=1/8&zright=1/10->[{xleft'=-xleft+yleft-xleft^3,yleft'=-xleft-yleft+yleft^2,xright'=xright^2-xright*(xright^3+yright^3+zright^3),yright'=yright^2-yright*(xright^3+yright^3+zright^3),zright'=zright^2-zright*(xright^3+yright^3+zright^3)&true&true}]((-1+xleft)^2+(- 3/2+yleft)^2>1/4&!(xright>10|yright>5|zright<=-20)) End. End. ArchiveEntry "Benchmarks/Nonlinear/Product of Invariant 3-dim sphere and Invariant Clusters Example 4" ProgramVariables Real yleft; Real xleft; Real xright; Real zleft; Real yright; Real zright; End. Problem (xleft=1/4&yleft=1/8&zleft=1/10)&xright=1&yright=2&zright=3->[{xleft'=xleft^2-xleft*(xleft^3+yleft^3+zleft^3),yleft'=yleft^2-yleft*(xleft^3+yleft^3+zleft^3),zleft'=zleft^2-zleft*(xleft^3+yleft^3+zleft^3),xright'=yright*zright,yright'=xright*zright,zright'=xright*yright&true&true}@invariant(xleft^2+yleft^2+zleft^2 < 1, 5+yright^2=zright^2)](!(xleft>10|yleft>5|zleft<=-20)&!(xright=5&yright^2=27&zright^2=34)) End. Tactic "Scripted proof" unfold; dC("xleft^2+yleft^2+zleft^2 < 1", 'R=="[{xleft'=xleft^2-xleft*(xleft^3+yleft^3+zleft^3),yleft'=yleft^2-yleft*(xleft^3+yleft^3+zleft^3),zleft'=zleft^2-zleft*(xleft^3+yleft^3+zleft^3),xright'=yright*zright,yright'=xright*zright,zright'=xright*yright&true&true}](!(xleft>10|yleft>5|zleft<=-20)&!(xright=5&yright^2=27&zright^2=34))"); <( "Use": dC("5+yright^2=zright^2", 'R=="[{xleft'=xleft^2-xleft*(xleft^3+yleft^3+zleft^3),yleft'=yleft^2-yleft*(xleft^3+yleft^3+zleft^3),zleft'=zleft^2-zleft*(xleft^3+yleft^3+zleft^3),xright'=yright*zright,yright'=xright*zright,zright'=xright*yright&(true&true)&xleft^2+yleft^2+zleft^2 < 1}](!(xleft>10|yleft>5|zleft<=-20)&!(xright=5&yright^2=27&zright^2=34))"); <( "Use": dW('R=="[{xleft'=xleft^2-xleft*(xleft^3+yleft^3+zleft^3),yleft'=yleft^2-yleft*(xleft^3+yleft^3+zleft^3),zleft'=zleft^2-zleft*(xleft^3+yleft^3+zleft^3),xright'=yright*zright,yright'=xright*zright,zright'=xright*yright&((true&true)&xleft^2+yleft^2+zleft^2 < 1)&5+yright^2=zright^2}](!(xleft>10|yleft>5|zleft<=-20)&!(xright=5&yright^2=27&zright^2=34))"); QE, "Show": ODE('R=="[{xleft'=xleft^2-xleft*(xleft^3+yleft^3+zleft^3),yleft'=yleft^2-yleft*(xleft^3+yleft^3+zleft^3),zleft'=zleft^2-zleft*(xleft^3+yleft^3+zleft^3),xright'=yright*zright,yright'=xright*zright,zright'=xright*yright&(true&true)&xleft^2+yleft^2+zleft^2 < 1}]5+yright^2=zright^2") ), "Show": ODE('R=="[{xleft'=xleft^2-xleft*(xleft^3+yleft^3+zleft^3),yleft'=yleft^2-yleft*(xleft^3+yleft^3+zleft^3),zleft'=zleft^2-zleft*(xleft^3+yleft^3+zleft^3),xright'=yright*zright,yright'=xright*zright,zright'=xright*yright&true&true}]xleft^2+yleft^2+zleft^2 < 1") ) End. Tactic "Automated proof" autoClose End. End.