Hello,
I've a question concerning this code. Indeed this is an TLA+ algorithm that calculate x^5
in the model I've set v=8
Here is the error :
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a tlc2.tool.EvalException
:
The first argument of Assert evaluated to FALSE; the second argument was:
"Failure of assertion at line 16, column 13."
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 85, column 7 to line 90, column 79 in power5
1. Line 85, column 10 to line 85, column 18 in power5
2. Line 86, column 10 to line 87, column 62 in power5
Here is my code :
------------------------------- MODULE power5 -------------------------------
EXTENDS Naturals, Integers, TLC
CONSTANTS v
(*
--algorithm power5 {
variables a,b,c,d,e,f,g,h,i,j,k,l,m,o,p,x,z,aa,ab,ac,ad,ae,af,ag,ah,ai,aj,ak,al,am,ao,ap;
{
l0: skip;
x:= v;
l1: assert a=0 /\ b=0 /\ c=0 /\ d=0 /\ e=1 /\ f=0 /\ g=0 /\ h=5 /\ j=10 /\ k=10 /\ l=0 /\ m=20 /\ o=30 /\ p=60 /\ z=0;
l2: while(z < x){
l3: assert a=a+b+c+d+e /\ b=b+f+g+h /\ c=c+g+h /\ d=d+k /\ e=e+5 /\ f=f+l+m /\ g=g+o /\ h=h+20 /\ j=j+30 /\ k=k+20 /\ l=l+p /\ m=m+60 /\o=o+60 /\ p=p+120 /\ z=z+1;
};
l4: skip;
l5: assert a=0 /\ b=0 /\ c=0 /\ d=0 /\ e=1 /\ f=0 /\ g=0 /\ h=5 /\ i=0 /\ j=10 /\ k=10 /\ l=0 /\ m=20 /\ o=30 /\ p=60 /\ z=0
/\ aa=a /\ ab=b /\ ac=c /\ ad=d /\ ae=e /\ af=f /\ ag=g /\ ah=h /\ai=i /\ aj=j /\ ak=k /\ al=l /\ am=m /\ ao=o /\ ap=p;
l6: while(z<x){
l7: assert aa=a /\ ab=b /\ ac=c /\ ad=d /\ ae=e /\ af=f /\ ag=g /\ ah=h /\ai=i /\ aj=j /\ ak=k /\ al=l /\ am=m /\ ao=o /\ ap=p /\ a=a+b+c+d+e /\ b=b+f+g+h /\ c=c+i+j /\ d=d+k /\ e=e+5 /\ f=f+l+m /\ g=g+o /\ i=i+o /\ h=h+20 /\ j=j+30 /\ k=k+20 /\ l=l+p /\ m=m+60 /\ o=o+60 /\ p=p+120 /\ z=z+1;
l9: skip;
l10: assert aa=a /\ ab=b /\ad=d /\ ae=e /\af=f /\ ag=g /\ ah=h /\ ai=i /\ aj=j /\ ak=k /\ al=l /\ am=m /\ ao=o /\ ap=p;
};
l11: skip;
}
}
*)