search

ericpony / polynomial-loop-invariant-synthesis

Loop invariant synthesis for annotated probabilistic loops
GNU General Public License v2.0
3 stars 2 forks source link

Returns "Invariant does not exists" #2

Open trivedi-nitesh opened 2 years ago

trivedi-nitesh commented 2 years ago

Works well for random-walk but returns "Invariant does not exists" for others(Ex: binomial). Below is the tail of output generated in my case(with verbose= 100): LCM: 30 Token (JSified): 30((3/5)(1)+(-3/5)Math.pow(1,2)+(1/5)(0)(1)+(-3/10)(2)+(3/10)Math.pow(2,2)) Token (JSified): 30((-1/5)(1)+(6/5)Math.pow(1,2)+(-2/5)(0)(1)+(-2/5)(2)+-1(2)(1)+(2/5)Math.pow(2,2)) Token (JSified): 30((-12/5)(1)+(12/5)Math.pow(1,2)+(-3/10)(0)(1)+(6/5)(2)+(-3/2)(2)(1)+(-1/2)(2)(0)+(3/10)Math.pow(2,2)) Token (JSified): 30((13/10)(1)+(-13/10)Math.pow(1,2)+(1/10)(0)(1)+(-2/5)(2)+(1/2)(2)(1)+(1/2)(2)(0)+(-1/10)Math.pow(2,2)) Token (JSified): 30(3+(6/5)(1)+(-21/5)Math.pow(1,2)+(-5/2)(0)+(19/10)(0)(1)+(1/2)Math.pow(0,2)+(-21/10)(2)+(3/2)(2)(1)+(1/2)(2)(0)+(3/5)Math.pow(2,2)) Token (JSified): 30(-3+(3/5)(1)+(12/5)Math.pow(1,2)+4(0)+(-9/5)(0)(1)+-1Math.pow(0,2)+(6/5)(2)+(-6/5)Math.pow(2,2)) Token (JSified): 30((2/5)(1)+(-2/5)Math.pow(1,2)+(-1/5)(0)(1)+(4/5)(2)+1(2)(1)+(-4/5)Math.pow(2,2)) Token (JSified): 30(1+(-8/5)(1)+(3/5)Math.pow(1,2)+(-3/2)(0)+(3/10)(0)(1)+(1/2)Math.pow(0,2)+(-1/30)(2)+(-1/2)(2)(1)+(-1/2)(2)(0)+(8/15)Math.pow(2,2)) Token (JSified): 30((-3/5)(1)+(3/5)Math.pow(1,2)+(-1/5)(0)(1)+(2/15)(2)+(-2/15)Math.pow(2,2)) Token (JSified): 30((7/10)(1)+(-7/10)Math.pow(1,2)+(2/5)(0)(1)+(-1/10)(2)+(1/10)Math.pow(2,2)) Token (JSified): 30((3/5)(0)+(-3/5)Math.pow(0,2)+(1/5)(0)(0)+(-3/10)(2)+(3/10)Math.pow(2,2)) Token (JSified): 30((-1/5)(0)+(6/5)Math.pow(0,2)+(-2/5)(0)(0)+(-2/5)(2)+-1(2)(0)+(2/5)Math.pow(2,2)) Token (JSified): 30((-12/5)(0)+(12/5)Math.pow(0,2)+(-3/10)(0)(0)+(6/5)(2)+(-3/2)(2)(0)+(-1/2)(2)(0)+(3/10)Math.pow(2,2)) Token (JSified): 30((13/10)(0)+(-13/10)Math.pow(0,2)+(1/10)(0)(0)+(-2/5)(2)+(1/2)(2)(0)+(1/2)(2)(0)+(-1/10)Math.pow(2,2)) Token (JSified): 30(3+(6/5)(0)+(-21/5)Math.pow(0,2)+(-5/2)(0)+(19/10)(0)(0)+(1/2)Math.pow(0,2)+(-21/10)(2)+(3/2)(2)(0)+(1/2)(2)(0)+(3/5)Math.pow(2,2)) Token (JSified): 30(-3+(3/5)(0)+(12/5)Math.pow(0,2)+4(0)+(-9/5)(0)(0)+-1Math.pow(0,2)+(6/5)(2)+(-6/5)Math.pow(2,2)) Token (JSified): 30((2/5)(0)+(-2/5)Math.pow(0,2)+(-1/5)(0)(0)+(4/5)(2)+1(2)(0)+(-4/5)Math.pow(2,2)) Token (JSified): 30(1+(-8/5)(0)+(3/5)Math.pow(0,2)+(-3/2)(0)+(3/10)(0)(0)+(1/2)Math.pow(0,2)+(-1/30)(2)+(-1/2)(2)(0)+(-1/2)(2)(0)+(8/15)Math.pow(2,2)) Token (JSified): 30((-3/5)(0)+(3/5)Math.pow(0,2)+(-1/5)(0)(0)+(2/15)(2)+(-2/15)Math.pow(2,2)) Token (JSified): 30((7/10)(0)+(-7/10)Math.pow(0,2)+(2/5)(0)(0)+(-1/10)(2)+(1/10)Math.pow(2,2)) Token (JSified): 30((3/5)(0)+(-3/5)Math.pow(0,2)+(1/5)(0)(0)+(-3/10)(2)+(3/10)Math.pow(2,2)) Token (JSified): 30((-1/5)(0)+(6/5)Math.pow(0,2)+(-2/5)(0)(0)+(-2/5)(2)+-1(2)(0)+(2/5)Math.pow(2,2)) Token (JSified): 30((-12/5)(0)+(12/5)Math.pow(0,2)+(-3/10)(0)(0)+(6/5)(2)+(-3/2)(2)(0)+(-1/2)(2)(0)+(3/10)Math.pow(2,2)) Token (JSified): 30((13/10)(0)+(-13/10)Math.pow(0,2)+(1/10)(0)(0)+(-2/5)(2)+(1/2)(2)(0)+(1/2)(2)(0)+(-1/10)Math.pow(2,2)) Token (JSified): 30(3+(6/5)(0)+(-21/5)Math.pow(0,2)+(-5/2)(0)+(19/10)(0)(0)+(1/2)Math.pow(0,2)+(-21/10)(2)+(3/2)(2)(0)+(1/2)(2)(0)+(3/5)Math.pow(2,2)) Token (JSified): 30(-3+(3/5)(0)+(12/5)Math.pow(0,2)+4(0)+(-9/5)(0)(0)+-1Math.pow(0,2)+(6/5)(2)+(-6/5)Math.pow(2,2)) Token (JSified): 30((2/5)(0)+(-2/5)Math.pow(0,2)+(-1/5)(0)(0)+(4/5)(2)+1(2)(0)+(-4/5)Math.pow(2,2)) Token (JSified): 30(1+(-8/5)(0)+(3/5)Math.pow(0,2)+(-3/2)(0)+(3/10)(0)(0)+(1/2)Math.pow(0,2)+(-1/30)(2)+(-1/2)(2)(0)+(-1/2)(2)(0)+(8/15)Math.pow(2,2)) Token (JSified): 30((-3/5)(0)+(3/5)Math.pow(0,2)+(-1/5)(0)(0)+(2/15)(2)+(-2/15)Math.pow(2,2)) Token (JSified): 30((7/10)(0)+(-7/10)Math.pow(0,2)+(2/5)(0)(0)+(-1/10)(2)+(1/10)Math.pow(2,2)) EXPR (after): 4(I1(18)+I2(-6)+I3(18)+I4(-6)+I5(36)+I6(-72)+I7(12)+I8(32)+I9(-8)+I10(6))<=(I1(18)+I2(24)+I3(108)+I4(-36)+I5(36)+I6(-162)+I7(-48)+I8(92)+I9(-8)+I10(6))+3(I1(18)+I2(24)+I3(108)+I4(-36)+I5(36)+I6(-162)+I7(-48)+I8(92)+I9(-8)+I10(6))

Rule: 1<=0 EXPR (before): 1<=0 EXPR (sub-exp removed): 1<=0 EXPR (fraction power removed): 1<=0 LCM: 1 EXPR (after): 1<=0

Rule: I[2,0,1]<=(2) EXPR (before): (I1((3/5)((1))+(-3/5)*((1))2+(1/5)((0))((1))+(-3/10)((2))+(3/10)((2))2)+I2((-1/5)((1))+(6/5)*((1))2+(-2/5)((0))((1))+(-2/5)((2))+(-1)((2))((1))+(2/5)((2))2)+I3((-12/5)((1))+(12/5)*((1))2+(-3/10)((0))((1))+(6/5)((2))+(-3/2)((2))((1))+(-1/2)((2))((0))+(3/10)((2))2)+I4((13/10)((1))+(-13/10)*((1))2+(1/10)((0))((1))+(-2/5)((2))+(1/2)((2))((1))+(1/2)((2))((0))+(-1/10)((2))2)+I5((3)+(6/5)((1))+(-21/5)*((1))2+(-5/2)((0))+(19/10)((0))((1))+(1/2)((0))2+(-21/10)((2))+(3/2)((2))((1))+(1/2)((2))((0))+(3/5)((2))2)+I6((-3)+(3/5)((1))+(12/5)*((1))2+(4)((0))+(-9/5)((0))((1))+(-1)((0))2+(6/5)((2))+(-6/5)((2))*2)+I7((2/5)((1))+(-2/5)((1))2+(-1/5)((0))((1))+(4/5)((2))+(1)((2))((1))+(-4/5)((2))2)+I8((1)+(-8/5)((1))+(3/5)*((1))2+(-3/2)((0))+(3/10)((0))((1))+(1/2)((0))2+(-1/30)((2))+(-1/2)((2))((1))+(-1/2)((2))((0))+(8/15)((2))*2)+I9((-3/5)((1))+(3/5)((1))2+(-1/5)((0))((1))+(2/15)((2))+(-2/15)((2))2)+I10((7/10)((1))+(-7/10)*((1))2+(2/5)((0))((1))+(-1/10)((2))+(1/10)((2))2))<=(2) EXPR (sub-exp removed): (I1((3/5)(1)+(-3/5)*(1)2+(1/5)(0)(1)+(-3/10)(2)+(3/10)(2)2)+I2((-1/5)(1)+(6/5)*(1)2+(-2/5)(0)(1)+(-2/5)(2)+-1(2)(1)+(2/5)(2)2)+I3((-12/5)(1)+(12/5)*(1)2+(-3/10)(0)(1)+(6/5)(2)+(-3/2)(2)(1)+(-1/2)(2)(0)+(3/10)(2)2)+I4((13/10)(1)+(-13/10)*(1)2+(1/10)(0)(1)+(-2/5)(2)+(1/2)(2)(1)+(1/2)(2)(0)+(-1/10)(2)2)+I5(3+(6/5)(1)+(-21/5)*(1)2+(-5/2)(0)+(19/10)(0)(1)+(1/2)(0)2+(-21/10)(2)+(3/2)(2)(1)+(1/2)(2)(0)+(3/5)(2)2)+I6(-3+(3/5)(1)+(12/5)*(1)2+4(0)+(-9/5)(0)(1)+-1(0)2+(6/5)(2)+(-6/5)(2)2)+I7((2/5)(1)+(-2/5)*(1)2+(-1/5)(0)(1)+(4/5)(2)+1(2)(1)+(-4/5)(2)2)+I8(1+(-8/5)(1)+(3/5)*(1)2+(-3/2)(0)+(3/10)(0)(1)+(1/2)(0)2+(-1/30)(2)+(-1/2)(2)(1)+(-1/2)(2)(0)+(8/15)(2)2)+I9((-3/5)(1)+(3/5)*(1)2+(-1/5)(0)(1)+(2/15)(2)+(-2/15)(2)2)+I10((7/10)(1)+(-7/10)*(1)2+(2/5)(0)(1)+(-1/10)(2)+(1/10)(2)2))<=2 EXPR (fraction power removed): (I1((3/5)(1)+(-3/5)*(1)2+(1/5)(0)(1)+(-3/10)(2)+(3/10)(2)2)+I2((-1/5)(1)+(6/5)*(1)2+(-2/5)(0)(1)+(-2/5)(2)+-1(2)(1)+(2/5)(2)2)+I3((-12/5)(1)+(12/5)*(1)2+(-3/10)(0)(1)+(6/5)(2)+(-3/2)(2)(1)+(-1/2)(2)(0)+(3/10)(2)2)+I4((13/10)(1)+(-13/10)*(1)2+(1/10)(0)(1)+(-2/5)(2)+(1/2)(2)(1)+(1/2)(2)(0)+(-1/10)(2)2)+I5(3+(6/5)(1)+(-21/5)*(1)2+(-5/2)(0)+(19/10)(0)(1)+(1/2)(0)2+(-21/10)(2)+(3/2)(2)(1)+(1/2)(2)(0)+(3/5)(2)2)+I6(-3+(3/5)(1)+(12/5)*(1)2+4(0)+(-9/5)(0)(1)+-1(0)2+(6/5)(2)+(-6/5)(2)*2)+I7((2/5)(1)+(-2/5)(1)2+(-1/5)(0)(1)+(4/5)(2)+1(2)(1)+(-4/5)(2)2)+I8(1+(-8/5)(1)+(3/5)*(1)2+(-3/2)(0)+(3/10)(0)(1)+(1/2)(0)2+(-1/30)(2)+(-1/2)(2)(1)+(-1/2)(2)(0)+(8/15)(2)*2)+I9((-3/5)(1)+(3/5)(1)2+(-1/5)(0)(1)+(2/15)(2)+(-2/15)(2)*2)+I10((7/10)(1)+(-7/10)(1)2+(2/5)(0)(1)+(-1/10)(2)+(1/10)(2)2))<=2 LCM: 30 Token (JSified): 30((3/5)(1)+(-3/5)Math.pow(1,2)+(1/5)(0)(1)+(-3/10)(2)+(3/10)Math.pow(2,2)) Token (JSified): 30((-1/5)(1)+(6/5)Math.pow(1,2)+(-2/5)(0)(1)+(-2/5)(2)+-1(2)(1)+(2/5)Math.pow(2,2)) Token (JSified): 30((-12/5)(1)+(12/5)Math.pow(1,2)+(-3/10)(0)(1)+(6/5)(2)+(-3/2)(2)(1)+(-1/2)(2)(0)+(3/10)Math.pow(2,2)) Token (JSified): 30((13/10)(1)+(-13/10)Math.pow(1,2)+(1/10)(0)(1)+(-2/5)(2)+(1/2)(2)(1)+(1/2)(2)(0)+(-1/10)Math.pow(2,2)) Token (JSified): 30(3+(6/5)(1)+(-21/5)Math.pow(1,2)+(-5/2)(0)+(19/10)(0)(1)+(1/2)Math.pow(0,2)+(-21/10)(2)+(3/2)(2)(1)+(1/2)(2)(0)+(3/5)Math.pow(2,2)) Token (JSified): 30(-3+(3/5)(1)+(12/5)Math.pow(1,2)+4(0)+(-9/5)(0)(1)+-1Math.pow(0,2)+(6/5)(2)+(-6/5)Math.pow(2,2)) Token (JSified): 30((2/5)(1)+(-2/5)Math.pow(1,2)+(-1/5)(0)(1)+(4/5)(2)+1(2)(1)+(-4/5)Math.pow(2,2)) Token (JSified): 30(1+(-8/5)(1)+(3/5)Math.pow(1,2)+(-3/2)(0)+(3/10)(0)(1)+(1/2)Math.pow(0,2)+(-1/30)(2)+(-1/2)(2)(1)+(-1/2)(2)(0)+(8/15)Math.pow(2,2)) Token (JSified): 30((-3/5)(1)+(3/5)Math.pow(1,2)+(-1/5)(0)(1)+(2/15)(2)+(-2/15)Math.pow(2,2)) Token (JSified): 30((7/10)(1)+(-7/10)Math.pow(1,2)+(2/5)(0)(1)+(-1/10)(2)+(1/10)Math.pow(2,2)) Scalar: 30(2) EXPR (after): (I1(18)+I2(-6)+I3(18)+I4(-6)+I5(36)+I6(-72)+I7(12)+I8(32)+I9(-8)+I10*(6))<=60

Point (2 0 1) failed New constraint: s.add(And(0<=(I1(18)+I2(-6)+I3(18)+I4(-6)+I5(36)+I6(-72)+I7(12)+I8(32)+I9(-8)+I10(6)), Implies(1>0, 4(I1(18)+I2(-6)+I3(18)+I4(-6)+I5(36)+I6(-72)+I7(12)+I8(32)+I9(-8)+I10(6))<=(I1(18)+I2(24)+I3(108)+I4(-36)+I5(36)+I6(-162)+I7(-48)+I8(92)+I9(-8)+I10(6))+3(I1(18)+I2(24)+I3(108)+I4(-36)+I5(36)+I6(-162)+I7(-48)+I8(92)+I9(-8)+I10(6))), Implies(1<=0, (I1(18)+I2(-6)+I3(18)+I4(-6)+I5(36)+I6(-72)+I7(12)+I8(32)+I9(-8)+I10(6))<=60))) Z3 Error: Traceback (most recent call last): File "/usr/local/lib/python3.8/site-packages/z3/z3.py", line 7029, in model return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx) File "/usr/local/lib/python3.8/site-packages/z3/z3core.py", line 3833, in Z3_solver_get_model _elems.Check(a0) File "/usr/local/lib/python3.8/site-packages/z3/z3core.py", line 1416, in Check raise self.Exception(self.get_error_message(ctx, err)) z3.z3types.Z3Exception: b'there is no current model'

During handling of the above exception, another exception occurred:

Traceback (most recent call last): File "", line 35, in File "/usr/local/lib/python3.8/site-packages/z3/z3.py", line 7031, in model raise Z3Exception("model is not available") z3.z3types.Z3Exception: model is not available

Invariant does not exists.

RedLog rules: ((0.25ny)<=I[x,y,n]) and ((n>0) impl (4I[x,y,n]<=I[x+y,y,n-1]+3I[x,y,n-1])) and ((n<=0) impl (I[x,y,n]<=(x)))

Profiling of binomial Building sample space: 0.01s Computing basis: 0.59s Guessing coefficients: 4.14s Random tests: 16.74s Total execution time: 21.51s No. of basis searchs: 2 No. of refinements: 9 No. of random tests: 46 Pre-expectation: 0.25ny Post-expectation: x Invariant: None

ericpony commented 2 years ago

Thanks for the report. The script did produce an invariant for the binomial test case last time I ran it. According to your log, the script generated a malformed z3py constraint (following the "New constraint:" line), and expectedly, Z3 failed to produce a new candidate invariant from this constraint. I am not sure why the constraint would be malformed in your execution --- a possible reason is that the versions of z3py and Redlog you used behave differently from those I used 7 years ago.

I have tried to run the script myself after seeing this report. Unfortunately, I could not build a working environment for the script after hours of efforts. If you would like me to debug this issue soon, could you please do me a favor and build a minimal working environment for me? You can create a virtual machine in VDI format, upload it to somewhere in the cloud, and mail the link to me. Thanks a lot.

trivedi-nitesh commented 2 years ago

Thankyou for your quick response. You can use my docker image uploaded on my docker hub account. You can simply pull the image using "docker pull nitesht/lagrange:v2". You might need to change print statements in main.js file as docker image contains python 3.8. Feel free to contact if you face any difficulty in setting up the environment with docker.