From bd75c7ab347598d7982937e55e55ed7ced85f005 Mon Sep 17 00:00:00 2001 From: Claudio Maggioni Date: Thu, 11 May 2023 21:52:22 +0200 Subject: [PATCH] more report work --- ReversalModel/reversal.pml.m4 | 4 ++-- ReversalModel/run.sh | 16 ++++++++++++++-- report.pdf | Bin 242680 -> 243736 bytes report.tex | 28 +++++++++++++++++++++++++++- 4 files changed, 43 insertions(+), 5 deletions(-) diff --git a/ReversalModel/reversal.pml.m4 b/ReversalModel/reversal.pml.m4 index e9d2c3c..8ceedc1 100644 --- a/ReversalModel/reversal.pml.m4 +++ b/ReversalModel/reversal.pml.m4 @@ -22,12 +22,12 @@ proctype ThreadedReverser(int from; int to; int n) { int k; for (k: from .. (to - 1)) { - printf("r_p[%d] = a[%d]\n", LENGTH - k - 1, k); r_p[LENGTH - k - 1] = a[k]; + printf("proc[%d]: r_p[%d] = a[%d]\n", n, LENGTH - k - 1, k); } - printf("proc[%d]: ended\n", n); done[n] = true; + printf("proc[%d]: ended\n", n); } // SequentialReverser implementation diff --git a/ReversalModel/run.sh b/ReversalModel/run.sh index 5f591df..d82dc13 100755 --- a/ReversalModel/run.sh +++ b/ReversalModel/run.sh @@ -21,11 +21,23 @@ cd "$compile_dir" echo "Compiling in: $compile_dir" +if [ "$PRINTF" == "true" ]; then + defs="-DPRINTF " +else + defs="" +fi + m4 -DN="$2" -DLENGTH="$3" -DR="$4" -DLTL="$1" reversal.pml.m4 > "$filename" spin -a "$filename" -"$cc" -Wno-format-overflow -o "$pan_name" pan.c - +"$cc" -Wno-format-overflow $defs -o "$pan_name" pan.c "./$pan_name" -a -N "$1" +# Execute trail if check fails +if [ -f "$filename.trail" ]; then + echo "FAILED" >> /dev/stderr + "./$pan_name" -S -N "$1" "$filename.trail" +fi + cd "$SCRIPT_DIR" +echo "Compiling in: $compile_dir" rm -rf "$compile_dir" diff --git a/report.pdf b/report.pdf index aa5400a0369437a0f880e56f98e2403001d8dca8..83855f949677201a60385d28335b68e6b81852f8 100644 GIT binary patch delta 10769 zcmai(WlSAFyP$!CyB90&ZU=XFcXx+V+&O4*D=x*|-L*h*hvM!|acBG8dv`b4Kby>t zXWon@^CmNS-lrqf^lQ|*dK@Tr-n7IN04?~!z!9|GhVgM}oDa(*;?x*JtCpNh`mRFS zF8&Q=bzzH$V&=ldaj~H(u_+C2=>2i(S`ze!uYP}Hxg8=%yI^GJ+osHDCl-x=Q&tR;#$9iJI(}MdQ^5DD*9L-swW#?os1jSyn3=9Ih|)vwMrI`Y zLD~BfS#Ptsi@!9w4{bduT8)~a-G>I8W=S>vXta&5NB&(j2M+uuGJo0(!L%Lg;aw>3 z%RaBxOa4|bslluh;5%UX8jyC=!3eG~TK67RPaWhj4ZZ+Nx;v-e-&t>L`M9uB@-5PS zdOijr3FlG9nO~zyK@sa;1>)53b5(y=yDcrY(cdIPy2Ns;n9tR+o{q=i*Zi5>Y;Z!z z*_|ewk=4;R-UBTO-;^#A+%qfNYNiynBn?I*$WdBU z6!NB&bGq5?5DDRniD&e?eu?<*ufLjGYoMf?x+{ErC#SJxG=AK0S7oOegis{eUMiVC zZkHunsJoesnr}KH>;9^e%n5{Xy|qTf6z;cQZcFq#?e2^Lkr2 zdfJiQvLl*)6#SIGDp5wZvHbGDOCpc zpd3b;GBYo*J2}#~&o}1?#lTSI5EtSSRj^rJj$?Ps>jXXkR(IGU@y_g}S6cI&I@n!H z&+In}nv0lOQIhiTsfZT|VosrJo1DExpuLD0*dI~SCllJf_z&Uo~ zzK%ha(s=pWRZMMx=mzegHX&0dnZ>qqHfDRfj*8&+xOS#C5Je!t^xG zq&8@%(P^5Up@gAnj%oBdw1DKLU{dP!Bg2iH66-=Wvki&}7m?p417+@p`J)nknm%PD z1$2;zieC7a$=v5vX%}RF(#4m*@E9e)n|XDLzc7AFvg{s$h+0~$!Hw+(#s#C9nwQ<< z@C2VQXGxpj&#Bk~8rkiHx1Ho>wEym~%U8&aqpz2INf!TBBz5)~>A=!6WwR z+Ff5hlY1+GF_{W7VzV}Oy0o8$8RcBM4H`XhIAvW2=7Un^JY>EF6u@G5eV#eEi#4Kk zVn&ppqoi>KJca&xiBHlN@UY(R=##3ruMCgFw)c6)Y>&AfUR-HItt^+A!o5|e?}tmb z1N%!?c@Ur)s6(pVt&fp`>FEJ+#=Q}(qR+CPZd}VZvxK2-leiuLXy+7p2y$?wZr9TO^$L?Sxk|VS&xuB*jQ}&d|r!!)9Hp6akyizZB#;w;#_N zgmZwc+Q-q2t)6~cC}g2}$%OHP<~58J3#v`S1OXT7!9eL6SLm38SP=(Y>V*=I3*b-XLi-|dMoPPJ9|`N zR0Ks@*P$_2PVGYR6=(UOvSXG`x4U*!H|fW+8&)T;q*B&sRDDJI>CaNC>MMo|W+1rH zWABK|DkMeEz?u!J+KCKFRP4TNhCKckmw@Y4z44%H83G20L=yiJq6f_G7-2D zT}K@icZK=Xvn|}@d_qrkhOv~IyIpGuHXi2A_OG%oao-5y*9PWL1cH^lMnLx{Z83U` z{qh=~+dhT3mjmN6%Ohq_{W$wy6WmC-D4$aI$;%}EPzg$egDYFy|O%;<#hIakoI&ZB5F)nxrL*Krz0W395 z9Ts|aV@1(JzcI8kqUY>ItHAiIi{%_kXOyTr+*OOYQ;qf1anKt!bGOu7b~K*hHYpI* zG0w!=gE?4MDL?Gw=hN&roWtSKRndPdwyBEsUp5;?tyEvw@ssyU(%JlA@r%~zoH3vIZE9EgSWOoY3Yob4*gc7(A@vAQY>emU1LErW(XtQ;q^ugD;YfY;|8V<2Chr0dQ@ZTfm z4<-*XlFhLgdTy4)OeyS?mx)9#=E1l7??6`T`Gv*Iep(LVe)>s@SyEV@SGkv z6d7piMF>wi0HN+nFddE1lxk+!nfviX>JvNFID z5~3p9*W2+lL$prvx}GK;Z$OyP#i)ovbP=s8j0*|s5={eS&HYB2 zL*3$-LRBTBH&wgSW8LSw)l&kMJ;O0NB(U=Ob4OSVoO#FN6J=$>*n;kRqI6DW`pFNWz2Cr888 zYRuoyX#5jTN2%vtE2+Pn46s|xI7#|*@7VBBpFBI0;-Zu(1FqNnN=!!AbzpG*53Igo z*rNiwMTe=vWzdpsGz9{f0%;XECQ@NPZXc+C@P@!x3xL1&dF?5pG_9-Ntf}_2BOOf_ z#7zwSjVkC!1Zw2HXVMmi;jGH~(`BLAKDO3Hk5YKzUTN3*n>`oQBAHW+O84L@-`t-u zt#vroH&;+*rSRel=&3n{)3;^hEsc?|0aJ`0Tg1SW28YgyDyM>f8e6%VNbwSexR`Nq zy3jx$1$1l>ytx!>!6W)Rs;9HB28zy?xZ5B0RS*=-Axjz&+He&L*+sob)k}cloUkxP z(^u|+6>7mflYsP*=q4_fCELdD?xl_1c&wj5DAig;%Mxuw6dk^h-Rz9zKPi?Zc%j4A zfR+FR3P*0Q)D$qxdYRgy30pYAl%&-yZNi6Ibo7MARGzoDxyTX6==(u?RxLMAH^ZFL zRF4Ofv~HXN!=%VUJ@)f!Gkq+&R6m3r_Dhj?m8RXW-kSfQV^mk=udc<@J%#a28@S&? z6`T8(s}-;sqe+9+G0sS5lMz}OrLHM#&5Owfy*w}>{ruo19wNpI)>QYtnJDQ`dUUIw z)x9wF;h|w(1VzuY;T90H;gpD%@Y2yk3UI@3dN?RNQSeh~N2Rc-n(ipUX%)5sup2)! zk72D#z)_SmjF)k;fYjdZ&Am*ytceai;uMV8y`E#W%1uMb51^F!fvQn0dT-ym*=q<$GT3| z_;&A^`Eo_N5FH;G>P>J;qdS9VAtm-sBJ`oE6F2yXlT!9a3{vw&@k=_cxo0Q|-yIxW z#y4rvpuBGidiMe21NczBtS;fV^3#XmwfI~|#+n=+N&5GksdV5MyYrBp1P|0Bu{n4s z`~J^uw9>mR%Khh?{UxkB#A}>*DveKdfrPkpXsEW$C9Wa zP(Q$71EiD`0^8kzoI^W+{f;3H%;E6lk(&d}?P?R$2H9U&Cl|oO5+u*CM^s8YwTNJYHK*GB+Hs{jUt_p;j3gr$yf$wZQ4_U2~GVj?Z=GA6kMc4dO)D%3Mzdp`)f?`IoKlT zLvANPfxTMX@6_KpL9-Ln9r?9PnNH4b`>Ms;R*Dvj)New2jHza#aW)ojiHyyn9+%jG z)l>nxHl~0`w%U=Xs?y9-Dt#}*u_Cs(Sg70~eCV>s<9cP2U}TL>F<7A2zGBr5%^gBgROHmQ3vFBoZ}t$ONs z_Tc=sWYdZ zY~Lkgky#xVpblkFBq`RHrBMpY0huX?3HetmQ$a43`F`}~kAHkn*WnN2MCThkUrtJ* z-iY*X1FGI!GToX>h>awRMC}3~IEFkbMy#|NY{51Jl;A#aP`gHTg1G3r=c0Rb#wKyG zVzViXI8luK0sTb}IEK+Ea6jaV2bul4=Iiy%ZZ4i(=%=|&j;miN+!OWWX+~eRT(8pw z(whaxGDd^k{8LAYl0<^CgyEPda>%C`88&qV3bmcokO zMC{RiDbt1NJ5P7E(KyNmdljLqD883l&5@xQ!#|FljyX)Y;Mez@^<;jvMeb-=w_doP zEL=NKVr$GyxV%JR$`%_=)ZEtW$B)wCQ_wwF-!QlPlT_qa%_fb&tzFwx8rZ=5 zY@nnBy4BIAX$?Dnl+t7pjEb?MK1MLnk+H*21X0^UOV*@$U$(r1)oJcBNCeJ3EG?;N z2*D=s2Q9w8Z4kSCP+PR%UY&9*N)H2?6Xfe1VCiU}FDYA%cN2NDNY z-A$uAXR*K+E)G&wQjnP)qJRJ*i-M(-wVMqoCkJO5n=6109IGw}T4P1ucxPw}Barx; zrO|>bgKS~LQI?b>8ljsJ*drnjpJ}{RNY|-E4*gSRv%B;0@~4Dq2<@uVarmuoGu>sF zM9hyLsmPkWiE|QZQ1}!GUvM>jn+Ev*W(#VgrLi}S;}>IpIvA$PTYgK?4La*_rreG4 z)ir8uN-k3q10R&HJPfnYvJ(maAyY?Qa!e%*(O)WIEj3UX_4W}|l?1gw?9YI6&Cpz* zTmcBFBb#T|#iUV{9E6cj7h;HM!!h~>;T?*8c^f42x-=qtK3`6$xS3@>55=Ms#3?0t zwUPbQXst!y_Hsskty{O(A$lfSI?)JAg@>j*9S6r7g3TW+k2~gB|IWU|n9`biiN=}Q zh;4jTUwxFnE8vwfes{w=q$@UJce;jLfAmixpYM04B2pRy#`4`enQXr;B&4 z4q#UHN^9VErgQAFD(?Mlp*68#4=s5D*ApSn?sji0e}3V~r^}zk6qmPQ!d$H?xT=^m z&T!v(N3?XZaCLLBG!r!G~JAUD@26>(4f<-v;SdLBme^%ik-E!Hx{rCfMRD$`v<12 zABh0pe?9hA-xR>cKj3K9%K#w%1I|{P?0=9}n+G5wWMgGTWRbFUadji*Vdwn6+0D+$ z{Xf20-_dogCH14mxIg~yWx5w!#80IoJ{F~UK1FJ!RnGDwREpV_mWE>)4WpN{M_vfY z#AFM34<`?gBWhe|D7Ze}X>S0n8jV1GBxa<1=z(mi3&SszguWpN+OY&HBcDt?QleKR3#xsWj|}WHsaZhT16;MmP^k1H&qj|teB#O*2%YK- zlIol$(o&|JEM#kTYvYPs_)SfkqSXOyAbX@}MwzO$ouM-_6X8t!g)d?U_O~c|6CoNd zJN#HbK?HKWjiXtA6zu0<=0O6%9qO5G-Ttf%at}wYj+y2tWKZaTUSuj1Yc6?=5A7m`nC-=gmevGSgB7U%eh?tOp)%(2jI1riVby)DIG{#A9IhhmRrUxn+PV@^Ybz9?rZS zYC^=fJ|mo47dAp%SC`_Mn=ZWA+wg<5eL)}|NbN)>jC}HK1>$ys6%qljEWTtObG|!# zYwnjWtv~HF>{nQ*gTSB6LK@(m7Yl)R`#$2-MpZT>`M(?wSiZlBcc3PIVt@wdz2g_v zNgcD5Q4&H5i&3qdx)e;0NcrV_NCoiXD#;H%(~aXx;X;44?ub_|kh7Of6lD~WQmCQs zeYY-|%E-cNpVMDiZmF^PgF`MaNFG1Omx5gdj|Nc?Bfo=b9ZM^U>2U`hKr@B$;H>(6 zko>cOyEbR`sNYi4aQZX4KH3>LDqJ*h6UB76C;p}>Dbz)z%(A@br@`tKD?qtqdVACL zg6vOnIPZ7kE|k+)`L+wy7^f?g8_!ar%^D`|U-!e&G6?kP72cNeeS}Q2BER9pjGcE) z%ob1#X!&&|X3Oz2$`BsBqsVHomani4m*nE%^AimzbeeVF(nxd2A#=p*d0+niu4$~2 z93k!p@-mwN4ee9!!dT^&fkC zq20_q8veZ}yftqA!zqWTah<^mmnC(+W`BO?#bRkC2Iwwf7ryd<>&@lT%uts2cT3$! zgsHB=a@Do~y{J}%7v<5$Yad!q8#s*)C>*}R6YEo=1>$!RrLimiCfr?Uol}=7h3?Q&(vfa4`cmL=2c{w!7)Q@8MUvW=@jWGl{>+6Z*R}8K5T|X2j>N{ z(dTj$WJ+J2Lt{$|cjbL_4HZ!@CmOVbCT-%!HKP<+FM8C^eQeCLd@di4G9H8*8>+-A zN|7F(*=v7mbkbA;JMiDoapMhT<@lYM>p12=)r2t6o3?nt9&R$`=jixo4{bJtRI&(q$N^sdAn~bcVJ|xkK%lAXi!o**li%4I- z{PA*2=3El~z&j>)&g;oB^pn}-W^5cDD*apMb$@5-4_A=0lQ3gP99D2&6l(ctVW|v z-eeUCofaq;5>KinEf&2YMMlYtz-Uamrlx#hV7`9q!Wq|q!P@8YSyE0@{w2a zFk>&)InO$nS>lAoG1w7XxSQRRap7>i8LCb#ruI~F!%VVCI1YO1)r)+z(bgtxe-<9S z=oQ`q?*llCDbC#UIpK9GGgSrdM=)(Tcv2{pju*&$`0X_D8Mnv_Ng=Ip?-h2A6J|=X zo%)hUELW43OyF#>u6SrU92QYFE~(K9koU`{GeqE~6PNK5(^g|>6{L)gfXxa{~;{PO;#*w`TP{4ki(5k)^JNEA^cxf5aT{bz>#|2d}(~js)x=y9(luIl{JrYk{ImjxEAhWt;X2qg79tgq zqd7^q&|gF)^L1O~E-bo{F^2WBD!wvm5nje~0Pchy^WGL&KMc!kI^y z!7S5?rWbo#CYwblt(1kPWNXdEm$Y2guKil}@t~Dl2wb|&f-l`}&?P1z&_`Xg1jIcH>Zaja2uSf**(v5+X{-9UdZ8ekXJ`cMkRumm2S)Se{j`ZXw1$W47Qgoc(e{P0vT|?39Is^&`K?cxWI` z1qqc75IW9~DP``;s1H05M|64_h?ud;n`ShyE+Af084`j)QO8$vD=TE-(Vg+2ZG^C7 zEaV?wwtre3hDkYw=i!2Kd!%pxYaM?hpzWeYhi>h$jZ3P)15#aR6_91x802`V2tb#b zP^y}$df%=2q*FeW^GytI_j!IS6zaP!5FwGEGH6Jx@L9rtQ5EC6Y+HRg+nlMvHl9Qm zn1impnXQCUG;FbozMpb1b*MtBX*eWL<${LlXeYuzZq6|wlZPEPrY}nY4`~$6&8(`r zq36f#tI9iDh<}yG5m);<4a7G&FIHI|GopKl- zyO01Zo=mipfRu-TKGsoX@X*t41Jr_FpN-+E_`Pn5^6!DdlcA!#@%f6j7nDE3CZID& zJ%pIv32V2dT}Z-uwye4zlgqoLH{S$)tJJP?V}MewA8CY1KA{nEj}|TWx4AGX zgBA;Rn{k1HC=^BZ2pP{c2_MvCgp#WlQ37W1%jOTEUmHtzq_(EdLj}XPS(fGD!DB{^ z+~?e>jcDfsj3ghL8cDlddVj1rDF~qoWqGR;3F?ExQgr?%2Bh*@AKh_V?Odt%PmK@7 z7}m*qJm0@Gq(iNKf~~;)={3vAio^3zTABr2R!eTBK*le2&h=+zQgd^UZAA5Fqh?b= z4e`+p^im|$K|bCXa1+bflhKvV`_4vwzkb~Q{i0QW>Y{~R^oRHnQTc>G_q*;IhE35&W;Fo2N53EqT2`_pioN zvn4&VS2#TV;kDUtGBSzFtEiRLRIo)6#_0(>N!=po)SN4g#jlM?SMb8Cy7db|U`DCy z>c1S>40dcrw*N8B!ks?11myVj;8Q#EbQ>+asd6nmS&IEglA1J&>);6gB?5cd8&bcx zby%Wfz5jct9a!AH!KuqjO*#txTPQc0XrA-uNrVY68gp-GN38S37KYld`igphi{Z?} z7)|fz&3t7k=*-XM<^EKhw;gCLmrLX$LJKXpc&hh3^4z60w4jwHS(Ys~yly$grPkqQ z_u%XZl=~z3ph=+Ii3_zbNqnf$=c?LooXbL6U}Y7Z2rReLa)Gd*wNqf4-A8Mr-XZcm z;!>2jHHJrZCA#LxS8{pjN{JX|n)EMdvRF#w8N9dhkAm6f;5D+&QuhkTJ5%PaglLO*Yoovh+({qjpBKgwP732lQrf6 z)uq!mTSDCiIS-3wnx9~;jcheDUdZWt?{^;*lfE@kEr$^)<&puH&}Y({r?;*?wY$bA z-#v=)$noV`S?U#rC>;j{IAkutHCxnC?R-!x23RcApF(T4$#-zJrn7dS-QG4g^5&we z3xTkpxSCMY*Aok~% z9N1?)ck-Bxuw~hiyf{_Vj!s$Lw(>f{uYF~Zu=ZKop85A6p4M3#LavoECXI||?B#}@eCh#>PGGB65^&>d z*O*Xk#h$fVRn?!XK6?+i$_+oO3yuz_nudWgy&!r|lZC74<3Cs$xr;#a=78vr#vXG^ zzu3j6r=@@@C*g}bFC6=p3Jo}|#@)q>zRKm?rRvu!p-TIbisw|kgvhTtDO+Fuv>3SVz{YNiSKTB6gOxl>);=*Gs0)km5q~|xk$mH)a1834`#-mXpF ze#*tCc<2^3vTu7|w-FKNXgyc)$?TR?+*VjDfUkf`E5&Pf4H1znO#(b5#*9{yd=s^4 z%9*QA*JmO2HqkYb)p8!}Jp|fC{x#yA0(nal+KuG^pKd>Ql#djUVHUtg(a+rx z?HG8y2z+Ykn4WYgrWz$+;JU{u`4p9)CeVK!U2OxN2*5F%O1{RI+HD$l33}#snNqH{ zM}R24dnWI-_984RCcUHa7F%?sL3Ti4LH$#7p1FWfXdo*)FzquJK=R*2o(G5puyL@b z)#U*Qzp(#r|G~!bfAj|%8~cCBJtq!ME)7-{R!%N0R`&gd`kgsXSte#WSVTOCu#mR% z^S)rR6qs_vm#IjqNZ#iYgBQrilX4NDREY`j<)fI2H^bWmgCios*o-*>iHje;V3S*z zN>jLr2d4zDteO-!&DKuIA*|dFZG{hk|BG7Ye@+cdE35~Qp>S{+BC@F4`dE^(ad4&0 z)&sB{IQ}Cd)eu=^ovc9rqMZNJlOWX>5EEtPkP?&R;Spn%WEW-S;^gF&l;Q^Ru(FAY zadL7=3X%T*hy2^`f9xg)7x#bL&98I3${MQJeScjy0TvP>ea@EZxcGRmII1FC&Zcmt z5G&4=GBy#aSP_X9h~$F`Y?SD-tZvxUlrrMGUjpOCf`dbIY6Bm^nZ_TF8?GRyzY-Et zf{FX=@S?mCFZx?yYS(??l<;LTB^T7F2zE{n9zh*LRs}X>T#KHD2H>s#3m8B5>7s9}S5dZ)H delta 9830 zcmai)MN}NXmWBfj!QI{68+UJlI|O%k_cZQqO>lR&PH=Y#5Zob<;O+z_^XBbm_x)G? zs>NO0Q>U^n(I0=KH#XtHa`Qs^ivdhvLj#wMZ+KrG8q@%+lu&XIE|Y>nvKa0sZ!E_I zzPlU?xHY20I{i%gRO__DmG>}Ds4!dAZ0)&KK<# z&&AHzK|{yU$JFJUMA7y!pAVj!5_m^x;1&oL)RYqn z5qJM$vBvVZb1GKBy5LrssYRw+V-L-d;;w;Cd;GzG7PrGI+p+_V$2C-UKpC~ab*Z=J zwoZ=7xBkqQLH?!*K#LC_9y_L=tBk6^$}yX`MWOBsM?*?3yMtClBSCA1D?FJ~a)UCf z*FU)Yhtcg!N=EJ z&PWl%O49=GVha9SFkOSD0VJ!x{EBbMl!S5M8CFgQ!dqgzgulAF? zO`qtkGAHKYQt7u!QM@D)Qfx|wZmC?%)3i}Rjm4~1ZR+JFziO%}x>MD2@TlN&Kxmr_ z$5i{Kg4DMD>}gYQVqX6B@((WvLm00dgbqq1HojaSxK}#+m{JQF%18JFk%V8&Ka2JG zkHxq`1ga8n9;pN*-wVqev}xSI$mRn~O-K&w3EM}tt|jj_+tWHX+(5*bq9xrO z#PUu@@(`;}(q(8<6P161JDDU+hNC7~tC-oOU2}}p(EC$}>)ui3G5=tJ1yQ6gr%%zg zvi--h(5V&H$PDzQbxdl;0c9A|%O6FCWrRsc^l))pvc7+5QAf(CsF8M5BO}(6{KY%P zvK0rOFj*u9Dbv#y+48iproY!uY2~o$F`JAcYi(U~nU`>#CX3ExqR;!wy(0PUduAAB zOCaB>f9>|#`fS{6ljfiTzU-KkKYif03aE7uDd;~M!}kE^>R>#3dA!SEs{U^FeST$c zx}B`vy3h;wlGSoA%-EMx6YLjtT_Ha6>vzGpH0%DDPU(APPdC2RtGR1&e<#zV2jae* zOyi-^Z6|*zLVm-;_~v#`zcXwNDs6F?^s1LoXSSa6%?sS|jLc8v1~xIJh}mhcS&VCc z9*KahFQOf(2bX`^z!a~~h)IPe_Pqg&4{sZzxVP(Mnz>@Hkf*VeLqCVwcecw~-}}y2 zwn4s@yHl*XL(Io8myZ$xhJT8TOXt^AoDQooD+zhMdgp?96h|{-UV@)mA5{zogCqi< zvHe*w3t;Sjvp;5-lvW3i;sdcz9v=27UDF&{Sc1fj6B5m&z|T+54nOL&^W&+}KlS;; z$NABE@3BbjK^ssyuke~idx9H2e4$=5x8c+4P_n1tf8x?xLJnL|;FhtA)yXazu9g66 zyPS9j)x{S12Rna9V{Xn^LR96EbwP3EGlqu!jg<4NVQiVSPus4Gg{l^NhlS!Tlju!i z3&ctR_9QIl!3KrZ`0#c7;~*p1dZo;<(?!N$st?vge~Eb{K7_Q0N~?IV5yFvIrtZ$~ zahrnRB_w9-2ScmvvfB;c+drUfe#_BUulHOe5NC?*cUwL4q#dV|au9LmSA;eqiS1Io z*Shps{oF$~F6;m-leD=~7=s2t_=5x?>N{Z{j=Usc!DB2^%s+0wje3VN%P4i>*S7++ z`b#4DvQjwAIcbJ_^x#E9=OO^zMrs6M*P(VCDs0@=2P{qf~PP)TS4cZFr&pC zWHtXdQ9ZCy88l21MuQmAb_81_)Pty9IEs5MBR;{CXI|ohH^8EPACaeiRNdX=<+Yq= z1TD1M0|#4$I2-2p&Cy@!8f5nvo+Jv(1pf);bRI~+M)qzv(@<(}uQ`i`BPcUf=(%LG zKU0YM+Pae2VWfIt;QxidD&!lTj9z#>E1vzhM9$O?uAe3Lvk0^~EBL04nrZ37bm927 zwA&u4ar$dih?PxYaz8L~Wrr$m(J`YV$mY`$V8Px&=oko+jJ9c$1vWJP!a7LQYq-}` z+AFLDOwgv8D;a*K-+d@~i#x^g!Oz|V?b9a%--X=CB_+Ik)%z(bi5K$Yzl4%WZNM`0 z#(%*MhsI1P^(>i6?SQ_dPu9Vt5vvm-s!0fRN1zY}qRhNx`kD8VjdnVf1$de^9ow06 z@`00ywp{KK;r!|RQt==KtkspI)9h4qQqf=hn;Keki~S<=rkxvPT?Q9l2AvG9PuI`X ze5o$ZqoyMx-9iGcjVr%oz`i#Y#b&{7$+|HlMPZW0y<+2*rN(!RGJ4Tz|GSJbAeSAE zE8d8)hLaB;nE*|wb-u)r*2IaI54nR!0LF0#Rxh~dTaJ}di@zE1LuNEg|X{h zFaV0`5fOeCe_EKCZV9DCLWScJ>b zA4_5|C?!ZQrNbOmVfxB8gM60Gz2^-%cfr@=JKtV%&6!FcQdQnc=7VnM2Fp;o1kqx4 z#s{ay#B8}i?*!cQ7;EuY;OY21GaXbhTNe7|(icHY+;_MB91lrzVvPMA4nutrG{5&Z zDLRH=MYNflYV8(3Mw;HuQnnfMEWID#9`%nJb!-hVK)OqY#x8WqzLUF`)YS0)rsr?% zTQwoH7WY}SNC~9=YXV!=9>)gtU(gvFa+U%uwZBiScQK=t9Cc{7ty_GZg?3WUYDD2a zeJ@+vnQ&n7urjq%*W$*1K>!%*-sRQtWQvr=e`@VbvBD*?=&zzQB)_vDmHin41;!8qxyyUj^2l{L3y6I6NC%(oDPrlzUH@zUrUXlP|1}Ym@`Rv579TYEO-AnJ;?$PDi|*674bQ_ z!-qV`u8prQ*B>xWrr4DcC6g)6i#uxBg>xc*R4e(xKxSU2A-ueHPIIpD%LwnVMyGeS z^)$iTbffmz$+*1EULwOR^;;emxmh>S95c6&E|I2z^7vhiCMRK+M}mbZ*et}V`sBl>$!fw)t4Ni&Q=mCY<#cbz6ZY$|xdzVF)Z(Z-85w+?fN&*Om z)rY&DYK1#9vB(SGxVfGh@Q~EWL%G4J5sKiw7CsJ^!jr&iK+1X5! zuiuruXQw&&0itAA-4FKdyIP3#!$wPQdi3MMw@uXveIzqacohHX_$ z;#=w{d6;o2&giTZFehRFl3nbe@R(PE4Q-+{Da|ASBm^4D>#Ll~8Pgp$vf+JHe`y>H zCyk7?D0RcxkpOEN6+U3MEH6X*Z#$Xi4DHGrQcE_-?i<7ZH_X{S@J~&QHp#@C{CDfb zVA12M4aNLRt$hCva^WM6p2Fkn&J|45VO{U;sj(wi-7lHoE&VNW65Q_PH+Kt#tD`m5 z5u>tvJmxy1D(4AtLDu)iol!{i5iCy_2(;lsG&DN#@!oNPC@xU3kS14KO|wQPq4K91 zk;NR2*<2dFHI8dN(d^EgxRIS*)6P@zNX9o7Traf4>bgeVhp!hI_$VpNfMBOpa^?hJ zKtkE6Wk?U$v%=EvM4v)pkGhN2LRgl3W15POB0enwDBOth~VpIniDK+DyeXD^N%l8K#t6*V7 z#n>#gcOLE!@3{&j*SM=zKikg*A7d0=4`*_;+kID!lQpjYNnyF*%rI;1_M<^2vInjn zC!7|X{Q0x=lDA4{SyqDdeqkLf)R86H@@#G9nhyZqxu&=Q(dRQjPue@ z=QcafwhOxU^VzN>KcXKJkPr+k_(ozyF6pqsSBE*YtZlA;#?4s@QbzrS3(YxwLFf$x>g4-#+-^afj-G}u$J3e3!CXcI9iyg zL~=)R1g^-dy-T*=|F2y_ml;}aQ;WP)O1u~zySZ3aawFAh$CQl{u75nRAH3VVFmgAlYu@J!t5)< z3jW6f2YP)D(_r~u18BP@>;y6l5cff!=@$ zSO{}BEDrS47oZLJ=aG^Hz=3K90v-SmYiS|?>`)f2VlWLBmx0=&_Bt5aR5Xy7=Q=)hbmCq3_t(?;t>8XRhk8u06^lS|Jj7* z0-j+Z_3{5Ox!@lHxPbhSv=%@(9FXT9k+cFR{*T030SPd?keOBh36UT_G6%@c-NTcT z|9?@*%Gt)#mXZeug!B~y*ui}5Z}leqNmtz#p}q*`o@&XdyNf7&lG7zI+7;r-T61k9EzgC6sXw%~`U4rX4RdPPm-6BDA z8JGv5A4xIwT@aA>xAac)5m}XR)ld-ZJ*m^(kR&2f*kPD=fqi<(4qmX#bbOz9)I4el zB$&b}5ZBgXWgL=+yoyPCcrQOEe{^meU9$a=!3Q8siJlIgA^Pz_D#riW9T29Tl!s;{ z4F?MOqGpQP!`35-@eLf>h)oClgz}11AZfotGswTgOU$aR^F0Kf>?=+TfGo8~um|QM z+W0s2n07#zTS8r5E?`2*Vhffo9rpWYjB)?OvNg0q8o85hm0SSOg=<)QF9^07k4MHL z`6Gg=$RzMMWLZgqR0M^h7M_80(iAg4{p%A9ZXEiMWf8k`p$u5jzr7J=fF7}6sxnM5 zL|aNKg}5dhzb{hU%nVKK13_Z^DEy5pKy9=vSRM(;EuRe_N4g)U{@yB4(+Iy3$|*>M z<0QF6YnxkWR;5;0g3c7es)EGD30G>zFo4#NgU4g-Rfs8yLFXpvX~iQwQp2sg?7qus;pU*oUCjqmYfQ&%cPcC*E(i^np9R8qp9DI>abwFehq6-M4v6S40*9yJ?l%L#Ib#Y6V4~7yMAFj~8Z)twfsGC%cMHp9| zZ~;^G=1k+WOXeI>J?`>HZg z%gm(Pm5+iHSWe|f&fUua9bBfjC%Y^nkj~dY@0W zSux_*XZCBRob-}CMSpb@m4|cX=2S5+fylyar6bQ^MO+E3whGV&&2LR6o|H+aJ+1bJ}4-@gwq?63%bYE~bmuY2ecM47~tBZq5jl5$Es z#Wknnc3hb-z8=k8%o7KmUiAIV%}&kE&L-l;_EiyP)~(tnpz_y7RA>A-U#F#~B;6`?w`=QG@Hmg=FL~AnXA|>D34R>8Q|C zsM+x~yqSv2u-tPURC>wLXDTvv%;}7WS|4IJ0*GAUchep^GH|pBdk`Xp>|pHXti1#_ zx3#UJz3U2FIW*SPI8;4}%b$V8z~cz>xS6%fkva>TtL+tZ*M{a;sC6L8ywB+i`08u( zjMe%u7^#hZC#cUV#jc+!i+RA8Sl2XiWwPd^vExJQsLAYU;iHJxl(cLob~DEx5N0Kj zj>i-eXb{iFPP&S*7I{92o5V7QC;b=w&rH=Tdj%6XtxknU*8-1-XG_BKOF;U*0sPydXA2~6;ozt z38Q*MK!wxM)u>jq85NR;_QzE0*)UBQoufuxN zIWaL_cBQL`Ot*xtE;|^eV5e@R6cy9``x;@a%0%+eA4BX{<{`E^i#E(gMdBEzcqkC1 z1=ng>4A(_FT6R|fPQHz6)ut3a|EjQ?ZV) zyb8sp*%WV*Q{eD)Vz0y=u;YYu2iMMlDz@j03D1tSYF&A%e+2zOq!QKB{#Mka^~r`0 zi22flCaj4*F*aF?d`dE52zuTLA5GX~YHZ;Z}j@bL`=|2#KyD<}mXQm`wz-}nKRqIr= zmm3~gg~lXw%SDjOYAf8z9t~`t%ahGrTpbzxm{G~-iVN$Ri8_o-CItxBrG?8U+D4Zv z1%i|%7ZrG9$Py-T(10lYOoZ}UpS8&Us*xoR39g1e5rRpZ^Tel*(Gw%h&j-yS*2WAP z&~~ZaKaG;D6N0%(M#`pi2t(zLceKU)wS(=}(A!ro%upOG3T)=v2%31QFn`pQGxq;5 zuwb(+D2ip<;&H#tR#%VGkP_#|wMOrSB9u_h|byZ)x!T^=r5J;PEvO z0cr(NE!d2hWngg0?-ka!zt&-!sGTb=t`Pp#NJgJ`!F}Xn-mG1^T0aKx9?Ng6IE@xX zc>sHYEk{q`;(JXw`d^s>rneeRKF^3XVzdN4%Bicy-T1E-V1f9;+o0~m%Y`a{7g2scu>xjkLo-920 z8gX66ezB(6Qe3~LYpyGd7I(Dgl$n_kAETTqLWZN};36mJIfmTUnt=w7CRbcJBU zxd!o<&S9|;=^(waX0ybX=o!hk_IQ5vd@=}CevT*jdsL)_BQDEt0ZoU zD_+Aw==`D`rMWyWhI7=Z_ax*d$u<{Qa!De|?@bl~8X?FHLFLJ|cLi7P8287ANy-tR z_O!I#jO@8NCe+6u$CK??b{OmKvvxAqg;7EldC}jxIe)NNcXGju{x&AUxv}3i6k`u_ z9Bna|+ETyP8v!Ze*(546@i!yanREMd=COH8(;fgnu{|9zI^mJ0a5V5=EjhfcX2)@H zMK01i4^*r!47tx6)qtTxR%F9^4Oj%${~XDmAEvBM2qZxA-Z$am__%j{13o5CTnmRX}&cq*rvI z?B5H0=mz>uj+K#=6BwPHm=Im4AD5aNRk^yynn1us5Zk!9EVyZMiRnHE_oY)aa5AAl ztb3**ZL+17!Mqcj%Y;E-oifYDhv6~ug~Z{Il0W*uNI&8;l5WG?@h|$i*YnmbR|%66 z?S=*WQ~d8jEr7bc^HyhZi-r{YW%&$I4xB*Q>a`FpKa8C2x4sV0@AA4>@;rChip>xe zFCQT&dBIXiA2_m%xL5gw#JG%Ke$j`)>qXrrZwXB?qnSacyIA{FqUO7Bok84%mj*wp zwv_>FFt2d3eQ(|8PWqkcSgr3W)ho1%L5fw*Wm;zvN4!jN`5UY(g~LMsacW6Phj*+=~k z-5A9F(-`USoTbY1v| zu|lcB01K0~d)c(!S%Y&mSCkz_FTkmJ7om^%;beV~hB>T9q`<81uLLX%0dCsqS4c0V znb7j^gx59HGK-&ZHHd12LbN!;LFkDesq0qO@?_BhH$+yO$n}%M z+Q|pz(o)ir!Eh+CY=}jTjg&I%ZtpNf)KpqL2G<0qPgnvMcKKaj1-ZYP%gCIIrfe|$ z_;^NnY%>#~aoHC|%BYnRe0C^Bt|Se6z00j62{Sc-8W;w$4MtEa)p!KYp0h-%aw3^f zexPI4X5iC6##1ZD7HV&cQbRYPLef@4c||Ew+k3$dtF%*nZkxrn?5Y#^+cLTc_mM<>RLKN{`zs zs<3xSqUU@Q^h`j&{k6mURm_|8T;Od=P(}AFRPa+jHETbxwh!a(-TC`&T>LA-(-5#6 VasdU9qX0PtIFae-WK}`P{{uM9tjz!b diff --git a/report.tex b/report.tex index cf23569..89cea15 100644 --- a/report.tex +++ b/report.tex @@ -233,7 +233,7 @@ termination \mintinline{c}{done[i]} is set to \mintinline{c}{true}. The actual thread-spawning part of the parallel reverser, i.e.\ class \textit{ParallelReverser} itself, is represented by the following -\textit{ProMeLa} code placed in the \texttt{init} section of the model: +\textit{ProMeLa} code placed in the \texttt{ParallelReverser proctype}: \begin{minted}{c} int n; @@ -377,6 +377,32 @@ ltl correctness_par { This property is clearly not generally true as the first thread may not complete the reversal process before the second thread terminates due to concurrency. +Here is the counterexample Spin provides to show that the property does not hold +for some executions with $N = 2$, $\text{LENGTH} = 3$ and $R = 2$: + +\begin{verbatim}program start +a[0]: 1 +a[1]: 0 +a[2]: 0 +sequential start +parallel start +r_s[2] = a[0] +r_s[1] = a[1] +r_s[0] = a[2] +proc[1]: started from=0 to=1 +proc[2]: started from=1 to=3 +proc[2]: r_p[1] = a[1] +proc[2]: r_p[0] = a[2] +proc[2]: ended +\end{verbatim} + +Indeed, the output shows that the second thread can terminate before the first +does. Here, the first thread (\texttt{proc[1]}) is just started but does not +manage to execute \mintinline{c}{r_p[2] = a[0]} before the second thread +terminates. Indeed, this is a realistic counterexample that could be reproduced +in the Java program. + + The citation \cite{tange_2023_7855617}.