[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "'Martin' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Thu, 8 Apr 2021 00:07:06 +0200*References*: <b79a0120-e9dc-4a1a-86b2-3141462718f1n@googlegroups.com> <C6A6BD7F-02BF-487D-A4E6-6E5E0C6BAA15@telecomnancy.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.8.1

Hello Christophe, I was checking for Termination (deadlock disabled). In my case it's line 12 which invalidates the assertion. I have an error trace in the bottom right box that shows the sequence of states that lead to this situation. All variables there are assigned the defaultInitValue which seems to contradict your assertion. In case you would like to know which conjunct was responsible, you could also split your assertion up into multiple ones. kind regards, Martin On 4/7/21 11:28 PM, 'Christophe MASSON' via tlaplus wrote: > > The error on line 85 concerns the assert of l1 "Failure of assertion at line 16, > column 13." > > >> Le 7 avr. 2021 à 23:00, Andrew Helwer <andrew.helwer@xxxxxxxxx> a écrit : >> >> What do the expressions at those lines say? >> >> On Wednesday, April 7, 2021 at 3:10:01 PM UTC-4 christoph...@xxxxxxxxxxxxxxxx >> wrote: >> >> 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; >> } >> } >> *) >> >> -- >> You received this message because you are subscribed to a topic in the Google >> Groups "tlaplus" group. >> To unsubscribe from this topic, visit >> https://groups.google.com/d/topic/tlaplus/pGbdbsDE8nM/unsubscribe >> <https://groups.google.com/d/topic/tlaplus/pGbdbsDE8nM/unsubscribe>. >> To unsubscribe from this group and all its topics, send an email to >> tlaplus+unsubscribe@xxxxxxxxxxxxxxxx >> <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/tlaplus/b79a0120-e9dc-4a1a-86b2-3141462718f1n%40googlegroups.com >> <https://groups.google.com/d/msgid/tlaplus/b79a0120-e9dc-4a1a-86b2-3141462718f1n%40googlegroups.com?utm_medium=email&utm_source=footer>. > > -- > You received this message because you are subscribed to the Google Groups > "tlaplus" group. > To unsubscribe from this group and stop receiving emails from it, send an email > to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx > <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/tlaplus/C6A6BD7F-02BF-487D-A4E6-6E5E0C6BAA15%40telecomnancy.net > <https://groups.google.com/d/msgid/tlaplus/C6A6BD7F-02BF-487D-A4E6-6E5E0C6BAA15%40telecomnancy.net?utm_medium=email&utm_source=footer>. -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a29dc9b6-78b8-aed4-5802-1e7893ac5010%40gmail.com.

**References**:**[tlaplus] Re: How to solve this error ?***From:*Andrew Helwer

**Re: [tlaplus] Re: How to solve this error ?***From:*'Christophe MASSON' via tlaplus

- Prev by Date:
**Re: [tlaplus] Re: How to solve this error ?** - Next by Date:
**Re: [tlaplus] How to solve this error ?** - Previous by thread:
**Re: [tlaplus] Re: How to solve this error ?** - Next by thread:
**Re: [tlaplus] How to solve this error ?** - Index(es):