From 505cddcf80b0c320497d7c280d04a7a178b110a5 Mon Sep 17 00:00:00 2001
From: Jorge Sousa Pinto <jsp@di.uminho.pt>
Date: Tue, 16 Apr 2024 18:24:28 +0100
Subject: [PATCH] updated selfstab-ring proofs

---
 .../selfstab-ring/why3session.xml             |  46 ++++++++++--------
 .../selfstab-ring/why3shapes.gz               | Bin 2080 -> 2057 bytes
 2 files changed, 27 insertions(+), 19 deletions(-)

diff --git a/examples/mutualExclusionToken/selfstab-ring/why3session.xml b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
index d367e96..3ef5669 100644
--- a/examples/mutualExclusionToken/selfstab-ring/why3session.xml
+++ b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
@@ -2,9 +2,8 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
-<prover id="0" name="Z3" version="4.11.2" timelimit="2000" steplimit="0" memlimit="10000"/>
+<prover id="0" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="10000"/>
 <prover id="1" name="Alt-Ergo" version="2.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="2" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="whyml" proved="true">
 <path name=".."/><path name="selfstab-ring.mlw"/>
 <theory name="SelfStab_Ring" proved="true">
@@ -15,28 +14,37 @@
  <proof prover="1"><result status="valid" time="0.010000" steps="63"/></proof>
  </goal>
  <goal name="trans&#39;vc" expl="VC for trans" proved="true">
- <transf name="unfold" proved="true" arg1="inv">
+ <transf name="unfold" proved="true" arg1="refn">
   <goal name="trans&#39;vc.0" expl="VC for trans" proved="true">
-  <transf name="split_vc" proved="true" >
-   <goal name="trans&#39;vc.0.0" expl="postcondition" proved="true">
-   <proof prover="0" memlimit="2000"><result status="valid" time="0.016890" steps="93037"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.1" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.054959" steps="311714"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.2" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
-    <goal name="trans&#39;vc.0.2.0" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.098094" steps="786750"/></proof>
+  <transf name="unfold" proved="true" arg1="inv">
+   <goal name="trans&#39;vc.0.0" expl="VC for trans" proved="true">
+   <transf name="split_all_full" proved="true" >
+    <goal name="trans&#39;vc.0.0.0" expl="postcondition" proved="true">
+    <proof prover="1" timelimit="1"><result status="valid" time="0.684964" steps="32013"/></proof>
+    </goal>
+    <goal name="trans&#39;vc.0.0.1" expl="postcondition" proved="true">
+    <proof prover="1" timelimit="1"><result status="valid" time="0.006760" steps="8"/></proof>
+    </goal>
+    <goal name="trans&#39;vc.0.0.2" expl="postcondition" proved="true">
+    <proof prover="0" timelimit="2000"><result status="valid" time="0.268627" steps="1869273"/></proof>
+    </goal>
+    <goal name="trans&#39;vc.0.0.3" expl="postcondition" proved="true">
+    <proof prover="1" timelimit="1"><result status="valid" time="0.642479" steps="24855"/></proof>
     </goal>
-    <goal name="trans&#39;vc.0.2.1" expl="postcondition" proved="true">
-    <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="1.802033" steps="24736809"/></proof>
+    <goal name="trans&#39;vc.0.0.4" expl="postcondition" proved="true">
+    <proof prover="0" memlimit="1000"><result status="valid" time="0.019313" steps="79453"/></proof>
+    </goal>
+    <goal name="trans&#39;vc.0.0.5" expl="postcondition" proved="true">
+    <proof prover="0" memlimit="1000"><result status="valid" time="0.068119" steps="356952"/></proof>
+    </goal>
+    <goal name="trans&#39;vc.0.0.6" expl="postcondition" proved="true">
+    <proof prover="0" timelimit="2000"><result status="valid" time="3.269355" steps="36850612"/></proof>
+    </goal>
+    <goal name="trans&#39;vc.0.0.7" expl="postcondition" proved="true">
+    <proof prover="1" timelimit="1"><result status="valid" time="0.826097" steps="18109"/></proof>
     </goal>
    </transf>
    </goal>
-   <goal name="trans&#39;vc.0.3" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.461742" steps="384971"/></proof>
-   </goal>
   </transf>
   </goal>
  </transf>
diff --git a/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz b/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz
index af3bab52f0fb256b58ad06b50b5db85f30e56162..949c9cdc8956d3b862867f2e2f134088942d51d4 100644
GIT binary patch
literal 2057
zcmV+k2=@0MiwFP!00000|Ls~^izB-ce)q5N+eywLAXVuab`EP6OdHG|2utU2P<N}d
zW@kN{v9lrnKBY^yTWx!1JP-oQz>HfZ)lKzPm0F(p)33|JXZOt?mf!u;VfVQI>ryR$
z{qw@TbNl=KW9JX<%l+Z#j{dMXZr#_%u7;YAgVjfOSM!!_YuLKqYSz-yz`tJ9AC~>&
z({i_OpZvnzIa+7*QS(hCYC#|FFSTfC;@w>>NS}Mx()@bkevf)LyW>PoW;vbYbe7Y#
zOmaHO$>5LN5(jU&`#tDc1wJ!uiKyB{V|OIQx3$U4o5a1{xwU&Zc=ze)Up`GmLwr!M
zb^m^Rdgy-n`lV*$Hv8Sv;duYx=%arK+jUR7{Xe4bd6YIj5HO6$Hsr0q5CS-bps>7N
zd~~1P;r{se#qVp*YfgI~bVhO<hb;}ErRhWsdzPyg>mfPP5oRXg;{=vmZ$1_>Vs1Ne
zPUM1Vu|Bh{O5182$L)uSQiWP?CIVxCgWZ8M8lULIF)vdHrb`?5-97BOj~$J}o=(om
zn%k3aff|Nkhh~Vb&D0QGyLy=t5{mn?MQABC?KHH3ZDuy{&7xw~Gqb>^W?|T~Oi?Ae
zkOwx2svILEFUORe(w9RTRwfbE>n%ljQZaT*KdwfqcfGAC_*B6z_J|t9HvEP~pt8hm
zc$D_3O|)!XR%o2txZ{)CAMX9WdFaRqF)@kj#ka@9v3=ZkyCXHZP@Th~d+(>&81nj`
zwEW(^r))@cw6YHA6-`_d)dayPsuG<=W%7_5o$h9qYQPJ)_ylucLxbR%%Bco?j`<ZO
zBosmC(^P|?piDJjGqbD9sWLYUg;|)T8qDP3##FOcQ_W6N&6dSWwGCxggQ7da&>cZ$
zY6$9Ccf78L<l+vC?g)Y=X5A6Q+;-xeMdrLaLfIW*-W_4q9pU!w2-mwKOu8eSbw?-~
z8%(<+4BZiIriSRwyW=$_Boy~obVo2WF-uu9Gn@EkQ7OCQ|DyxY3sTCsw=VEM?gCfA
zjfFWN1eoZTfeV^)XcSe6zNNimfeB85#Q|94naaT89N240NGOCD3t%xQD1k*bGn@EI
zVDJoBEP%xsus8!2Zv+;u0t*vh;k><L*_N?r?>Mw~l$jcW8ru7U-qZcJ-M)K88<4N4
zf6o87o|T~hM>(75Q&wIP3fVj6BP4ooaNbjNQI~pJ+-m44I#WYW(evWIqJ)HEb?c(1
zgaVoM6g4xux_o%e&6?H4UY~o)d7Hm2_2kvmlathwKj<m3%0?h;qF>fi5GgMQQG`U_
zdSGCI3r@ks0bJCX8cJXe?lmPO6f3*{7Zpv+`ih#FO?<Pya0V_G;NlEioPmosf{Rzd
zMY(yqNWWdAf5MCO?CKmENc@uSb+_iXL-OsAyy1{sy&aN2*&&&~+m87B<lVsS_TOuH
zJ%wYnj?yyGFT6X3gdassqMuLU=RAtVFjfXn^b3nBWaB6*68+=b?BGp!@PRCkBz|@#
z?T*_zR82aWP{)&r9_eH{EvD~(h1iDQD4z~7QGWlM53&`hjZ8_OIO)rZBq@?fkxYu@
zB}KO#h`cxvpL|cnnI0)q^DwVW&>I#KAZhs}s9%<QB{t7M!!d@59+#nk@Hajd<#~!a
z*FS;=l0LvWG)RgtDT1U3E-8A&yUJZ!4?8?%eQIVjwHt=XpXAMHZf?IcM)G8UqMA*}
zTIC?mol?<}fK_JIwMnC#7(^!o%{hX))JCjxZMNpDP!}hDqmPtIM4V~0rPd%Z&*Pl6
z*+_Vohd)Zgac*GVjEOc?99dGB(p_h_-yQ!RfVlrgbcyH<Ym)+`YsKlW%9&~POYmwj
zmCAmWE(D))g`6*3b>R8MQxabC?!)L^2ukV-;byjp0K_9tmik{XUqqy!#OOg_A3_tx
zIVLJU<*8$hQyJFm8&Ae^$SyCQd-&|aG+a}n^t=q47{Z3h`s)7E-_je#dJ<VG=k~K}
z9{eg?sTav#UHbhYN{080fx%1!KZLvAVl<KCV$(Bxb$(J|BONtZ5;@t<%)C$wJUg0K
zp<E4B^SJk)!qJ>Lu;if3@?XCl|8pPzTVt`1-n6cFVA@VJy=2xf*|x2s8ELzYEurES
zTl5Z%=!_PPYZYsxYQalrMPs}YO!B3ukl3J+Mr+%eo`GsQuBFtCS00T8-7;8mthlTs
zv7*AJX{_uG>#(s_c&ECC>7F&ha4#aOh^)*qW<6TZP*}3gbgMenH>MF59rTeEB5TWN
zQ7hv}gH|9+XIqD;1$NMD&X>AUk&$cEx@p>uTiF=hFz3l_&S-zAkr`q%$xm!V*9w}W
z?K|fi&b4tuN^D!{wIoIx8MW)ck)2*EWvzs+k<NFTsn++xF-44=MNUa!YDL$yO;22`
z!Nxd>l;L0n_N)t>JaTr58T7_`=vvxG*P-?us?PA<_RPA`OJM;UCwk-BhTaGPMc09C
zy`>Fl6Zf6G?7i!`Z*+@oqk2zElA`Omc2Y_7&B;q)C?*Z<(Q%5k?xAnB0N*RG$b!Zt
zKn1)4R&iT#Q*n|^u_ZSEC_h@uMZ>*CYr+f)<vDp}mmn&@OOhQ!PGR80D;h-`bka#e
zz!?oKHgXB70(nW&XxRw@)wG@>-e_s8vC3+v0Towf38n&lNfO$=mn~f|D76SRpa^-_
n^~`rx2#Vhlb%m-zSs^7kRtOdH3RwmAlDhu_l<IQp2_*mk)?Nwm

literal 2080
zcmV+*2;cV~iwFP!00000|Ls}biyJu-fA?SEx7=+AsPwHPvtR<I4Q3XO(ED&4gSuON
zV=}P^+sW+x_g7L&c1v#0jPLGoA#qEpPyMPSl{A0(Wqx?H&+ah)>Gp@sZu_^nod5FI
znf+|H58GYm4))u_;b@QUFgvd8_gz=h8cvPHy}hfUCF`25?Z=w5NJ{+6S^Z_+@AmV}
zw%xm#y|YLs_*26wbZU-2_EXJU9Qb@!bJS-)w>Z9B*<XX+)#f;o6H!hLaw^KHS`2b(
zkQ3e?u|^JP!T##?EIgl1Q^H=YgRwi5f_1GU^J?H;Z|u@O9i08T|KWzAU<i_ewSC#`
zpSlm<zt!Y4&3>~#93P%6{`60Nx^}<W{ww$%Tf@Xtho%<Vrg17XK|s$CWR{mRd)(XY
z;lXX2r_R3E$JqvTe&77jZ~mD7<DVb)?(pO3_~FO)$H8^z%L1tw5Bmak=iA<7!Sn*2
zu-SSIp9)%#+1XF_5ux-<7|Lrl0@3b*wkr-nB=2DGh)%l%ulbb3b`;%;umtBGTQa-1
zkM{6z+<kLf`{MH=;_W-BHA*=#v|}cS#e2kSj-uEdB@?g3a&<pq=DDrFGZF|nUKo>O
zV=}cu{IQ$K%H`_Jo6^hMI>UjCCuQukB!_vP2`l^4K5e@Du4b56v2C{*iUanwKD(Dj
zvhHX->Y*J$)r<c^Tdn-GvjwYaJ;pfkO*j#_bHvng$_sPhg~_@D_$F6nM&Kv5!ilLc
zMA~*b7Ku80-W`tZZrg2+xED{wL0tGON(kPQ-0#%(cCIJB2`App`Y0?fypR)dcx4gX
z9EWRbB2mW+W0kK{GhU}=w9a*e-3;vryIH(Pyw+u=;Q?jxJw@lX7R3VbORd~ffQ+rd
zY2^=qVm}iHa@)S5uI(%844+ySTQacBB{rHAq*D+_hh93NSvjvON>C_FjE#W=JXBc@
zCD6j`z*oRQFW}^vSzf?d<T~)%-~_maC%_p{fTgc39>-ezz~1#~Jq;DYF!B;k#dtVg
zJ>^SXQ#Hcul`_Mh<%Nz@JupF=t|H!=#j2e4>d(yje`i+VmCC$Q<EhDnsEWOWs4Ay+
zMF|Rpxv30Mi30_qvM@XF6^O_SM0I9X7l;-+C+Hgy6;}}zBSgj0U!-nWtM;QWv}gBk
zFWAS^G8-0H>|ehKyvOjW^tN1Le<sBLoDjKJ6vkdr7)_0mbSZ?`i-=NKyiW-V`MFUT
zBTBu398pRNvjbm_2qh(=lxAjWjwmfQJxXsx)Lcc>j1V=r#12RIyxDdsnMYavTaokw
zM=pWoZTJ8rZogp;lyUyo0^@g@ap<L{PsCJpL+Yjc&kFBXl%P<^#H`u|?vv&mt-w~8
zT}&SlrCFJom8lu?|8o7D-zvoE2}4Xq%j=sir~_pbEw)^YFg|ZV$j9x+cyqz#l`Y7t
zGubrE7>iVagNeNq0#jmfMF|Q8FtS1%w9m3U1iCQ0nBGDPvy_a@Qj&*YV!_=Og6VoZ
zP(~q8uY@2JS+BxRSvCbW!hxP1u~_V-{fd=1Tv38T0f?-~q7(;m_|sN%GP{`GZ%VW0
zA}hVwh3Vh09pG{NbGS6$mcwt!O#z=|{0CBZjm^>PqgmrWTQj_st2JI*H^+7Dk5~Uh
z%5b^i*xG-F3;CHCDsarOwf`Sj)xfIO`J<Y5ZMi_To{0|n=viM>#843%6wyHuol=y)
ztKJRM9zADzBu0~C;iePleugJP3_cERQgiSp-8j-%X+JlH@@N22jV44bBgmywa(ODA
z23CbP@6d{gf&C$Z`Z9tl*XEzG3T?*U#K-Ewz(@QUQVBa3T1~FiOB4rT%GziI0Iwat
z<%YvpVqTpRZLB!33@|}Bpf=mh@pm7HhiB~P5xs$S3MTkN;ry3^$h7$2y_$`sqMx}7
z5N=Mv@k_#02i_*0lW@wrFDLIjD8sG*p?viL2sNw7^}l00LnQ0*lLwwXLF3yI6B)na
zyknh)VpyYZFc^!FO%pFYe3LMSYuw2_&tc;UHa1vaJbe8-c7o6uSzONTqivqtVz^BO
ze^u`HmmnD~3XwsN1i$!$cy=-oaWTW!7szK7CiH^_Usj%NM`p;>QizU5D$S{W)$F$J
zYkcVR94zO+%yQqKkN<uMe}S9Lgww6<E!Azun_dv3iD=ta;)pO^N9MGGip+Y;H1D+H
zjcp}qglwr3wB?O<k`n=QUNK~&jnGP&R`-O;rUNB}YMgXT8>(7D=M4EoC6LuROI_D$
z#(QA8k;<5^1qBTktWhlstSqn^Mi~(9C^#WagPt$~T=k@JhDpWd02PqRRJu}?3?jWi
z+rU)Qa7kNB0ev*qpefpP)^$NdRKP1>70{EM1WlY(Om?khM)0<$f|^d+z84%c_i|KJ
zlvk8hl#WG>(XL~*HLc~UrK+)}X;njd(NSYLnGmHoLMkv7=n7N?GOEI|qLl`ubR9=D
z8}y=64qb0KaoV+0s!T<-*F#lBlb+rXO_Y?}NRAP}kh%_mGqM+0!C2+>Fj_JECB<yG
zCe}5ra2814sGjz%;?(uhNk$N$Ij0qeij#_&is_1}ibcs@Q;ONq8sH6JgpBqhj7tZI
zgqd?*aW*B{5e6D4ATMtu!3tSe!B}IpqAhF0oXd)fDM_tF$3ZdOIwIRf32n5IMp;Ff
z1gYm-S6od=(iS7z;{C@+B4|f@hl$zs#C3*qLz=lzl|WWZT3!jvM_LJ}1gW^0QuiP3
Koy$Gj9smFzPY;Fw