From 577a7ec0a4e526227073a3388598c7600bf5aa6f Mon Sep 17 00:00:00 2001
From: Jorge Sousa Pinto <jsp@di.uminho.pt>
Date: Fri, 12 Apr 2024 16:08:24 +0100
Subject: [PATCH] updated selfstab-ring proofs

---
 .../selfstab-ring/why3session.xml             |  63 +++++++-----------
 .../selfstab-ring/why3shapes.gz               | Bin 2051 -> 1366 bytes
 2 files changed, 25 insertions(+), 38 deletions(-)

diff --git a/examples/mutualExclusionToken/selfstab-ring/why3session.xml b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
index fc65260..79299a0 100644
--- a/examples/mutualExclusionToken/selfstab-ring/why3session.xml
+++ b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
@@ -1,68 +1,55 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
+"https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
-<prover id="0" name="Z3" version="4.11.2" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="whyml" proved="true">
 <path name=".."/><path name="selfstab-ring.mlw"/>
 <theory name="SelfStab_Ring" proved="true">
  <goal name="incre&#39;vc" expl="VC for incre" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
+ <proof prover="1"><result status="valid" time="0.000000" steps="4"/></proof>
  </goal>
  <goal name="first_last_fl&#39;vc" expl="VC for first_last_fl" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="63"/></proof>
+ <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">
-  <goal name="trans&#39;vc.0" expl="VC for trans" proved="true">
-  <transf name="split_all_full" proved="true" >
-   <goal name="trans&#39;vc.0.0" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="1.20" steps="31957"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.1" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.01" steps="7"/></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" timelimit="300"><result status="valid" time="27.94" steps="125263123"/></proof>
-    </goal>
-   </transf>
-   </goal>
-   <goal name="trans&#39;vc.0.3" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.35" steps="5731"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.4" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.05" steps="93192"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.5" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.10" steps="233571"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.6" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="1.69" steps="10123015"/></proof>
+ <transf name="split_vc" proved="true" >
+  <goal name="trans&#39;vc.0" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.021446" steps="92842"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.1" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.058045" steps="341458"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.2" expl="postcondition" proved="true">
+  <transf name="split_vc" proved="true" >
+   <goal name="trans&#39;vc.2.0" expl="postcondition" proved="true">
+   <proof prover="0"><result status="valid" time="0.079543" steps="653987"/></proof>
    </goal>
-   <goal name="trans&#39;vc.0.7" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="1.62" steps="20200"/></proof>
+   <goal name="trans&#39;vc.2.1" expl="postcondition" proved="true">
+   <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="2.140096" steps="21941721"/></proof>
    </goal>
   </transf>
   </goal>
+  <goal name="trans&#39;vc.3" expl="postcondition" proved="true">
+  <proof prover="1" timelimit="1"><result status="valid" time="0.053541" steps="1378"/></proof>
+  </goal>
  </transf>
  </goal>
  <goal name="Refinement.initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="146"/></proof>
+ <proof prover="1"><result status="valid" time="0.020000" steps="146"/></proof>
  </goal>
  <goal name="Refinement.initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
- <proof prover="1"><result status="valid" time="0.10" steps="1196"/></proof>
+ <proof prover="1"><result status="valid" time="0.100000" steps="1225"/></proof>
  </goal>
  <goal name="Refinement.stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="27"/></proof>
+ <proof prover="1"><result status="valid" time="0.010000" steps="27"/></proof>
  </goal>
  <goal name="Refinement.stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="72"/></proof>
+ <proof prover="1"><result status="valid" time="0.010000" steps="72"/></proof>
  </goal>
  <goal name="oneToken" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
+ <proof prover="1"><result status="valid" time="0.010000" steps="23"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz b/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz
index 44bcb91203c5f5c914ef57c6bad22292a45f2191..af6e291cc95f37a38e0e2618fba02986afa22e73 100644
GIT binary patch
literal 1366
zcmV-c1*!TUiwFP!00000|CLr<YvVW+eb2A(TX&}nNLP|2E$u)l1O>tjEXDh<EJ0u1
zhG~<Mq|@1dzgL#**l9YQfnrO#=bU?VudL>`57qwOKE-|YE$;T~?dFfFu0H%evsZSr
z+H6DI+pnwr!5-p%c39fSZD^pO!{Fw#y>6%{%LbPAvLPNrJ$^oGZmV{?tJWL8i!*y|
zF;4K&&_y?CI6myhhI?GNx^6h?*(;Ch^M(D?=`PlX5l<AJ%sg3mvJsglGfyNxVu=Xq
zsr{66ZW2!QTf$kRx@6bLqRU1V@FJs^Ydg0O`)KcW&oM7`iD)mdv@hG;L%4YS+K^$J
z?RvLAtR5^r+K04VyIXJm?Yx&!-grNOeuTN9Yz6ufz_A3A%=4K&?CfU0iW~P3?2Emh
ztx@xF{k>g(um1k$Vi)(%4~L8A&GSA6^m2ny?1z1!cALg2<q7D8roeiW6h5BBI?mR9
zwD(xb1j1Inm7@#VZKw8zAzH#)njOJ;OY}#cdfFDyRw+wo?%tCbQoh-j{K~A^({_LG
z+f7&>@OY0Siyn;Bu~b^v#dcF*x!`%_B`3M=U+0T<s&%g9vmbOVmF7faDDRor`KG+L
zi^b`-hjLu~N;&LhIvTUj@7Lsh*h$_)nZJE>e<tzb)a|f~{UJWBH=)Omgua~UX2g`y
zi2S0oN8_+Wx)kZoIR=i_8iCi^Wx3OEcxvrOysjy4aMFwR(<Kf^caUD<pKTc4pmNzT
zyfl}M#5C!mWDRAwwoI>l*B*o2!D%4f-lXGGnW1ty{j`#``3=e@5M(_#>J=e|LM#hG
z7J_p^)7$krZ+mp9rAmx8$A$~G!=yve4bpZ8RJlrVY26RAx&Eu^*G|n$Gb4YVZ-|^i
zG<B)?sl$3coX!lD`0u3~l~aQA+)nknopP#%&{H+tP%@G07B2CT&lOHysp_d}V$4qt
zbveQ%38f8%FVn=`S`S_fr*16VL2{XJ#1m+J_$xJH^@Q_jdw(G|G!s?X=*L3=-CQJB
zvoWjqoLWep%IESr@TP(HgU1tj&fV?cE)^wT5jeo(lNx{nT%79v#QLNnlNlczBzRw%
zG%hu%%Uc|;uVJaQwRodBSt;51;A@BP2FB$YPo~bNW#fI>Sk8X4y89C+9qCwE{G9#0
zbr10dr#XN(*3|cH$3!Et2dEM87N_OYNGVEPbbbRFOXzOiDQKh|a~Ck3$O0`!OBANj
z^wn%P@oxJyZVG};5qPrV<I~~4RrjNOHWN{K+geaQaMuc=6%pS18dro4fmC3qA+y#p
z#e<UESzi+;Y7bF>=T60%6G1C(7{b5_C8hSNB~ZISr4Z7^Ix?j}dIA+A2DA|f4PJ20
zZE!BMfjZi1>m(4zbYK<)sVFhpC?ieX;W@KZND?Dsq19BiT)SEe1yn-R#3npth5~XZ
z9cYpS7F5faLvO;hH9EAwebmlbkTlT%3{a#288a1FLaYi7fVxnt*6PT-1V?M3DTCKc
zstv{D($LyaVJPoCa7K8`d5F&WHip(Y8NK2}5^$Qw*Gf<u5J?8O0aj$Z)=Ux|u@}+{
zL99TH8iK{fU`JdhqmqU^*$P+0M(0Jel(bH^(0a)swsou-v659x8de)748uM$!@w|_
znXLlAR(nmkqfs-h(hB2sqye<9m^MtEV+O*gqCgSLT}`yL!U}AIRT4aNqT<wWa*nB_
z2%Ji$d?dAZQYfu-t)-Q~YFev`GsEE=6MWkWPleSr5fGq_HrmjV7&PaaxJrN#2qlJV
Y!<FIE@Y--;I6o)%Kf4Ee2)hmd07|s5Pyhe`

literal 2051
zcmV+e2>kaSiwFP!00000|Lt1qiyONY|L(uS-_qW2LGMS&UN8YO3uX%?Oh1&eXe3S7
zWMeP3lfC`#dnC<68r#{~8`?|Tg~X%BdH!_Hkw&wB_-T23Fi-xt{N@kG?SA*CrC9#-
z$A$S|cK5rz^GEaf{&+Gce_Wh4=F8sIq{c&Ib!TpBY|*AB8}q(K7N&ao^`ic`Z1;!d
zc4rTMVQvh}BlxNDZS2$xe$3A`voP@Cre+||e6TRSzBRu@xwqR>#>YE8nfPSKCu^Sg
zWa8t&9=-tzY_a(z$XNwC)w=|}T190yz=b!p>WFU>^=50<=JDvwr^8pDhN2?e3)q<F
z{o&EQ`|`O)gPZO4a6H{V8u)1+gS+Oi-Tfol-nEkBeTVcd&`mm5NDl!SAt*Gj7kB2t
z9Pdy2&wf{9Tx0OPml?Z5JGj(C3&W|``^;Cf<p3YZ2qPJM7#54KZ|@2oHr1UdGrpjj
zt<Q9eQnwh|(fu$`iV*ADj9~yc=<O+^@=PWj;xa*yPu-et=5g!p9JGT^qj9{(dbBO{
z`eyJ@_2}xZ*Q2Xf^Mn9X^iLPiLTKt7+CVl@o9HH}sP#lGLAhGe`^*!n&@cE2%24G4
zLi{qOV3fQJX_(0nmFo?loMnvOz&}${$alG^0er|{6Kh0G*e3iBlLXR|Zo;F~4`srl
zb(x`Y?ADwPW_P^zyXMh>5iC<l*Ndn9@nrWqw>?3T3)y+_Z3w=^m3lnM0dcv`X+ZE|
zEqT5&Gt=$5ka@Yr$5i95$TVIg8XxnF&q%X50dXbA_;*t*WS}ndUl(;`W|n<d&b&m6
zbW`1PQVkgMT#MaF4f}4k&8%Tp5-v^^88-=8LW?>;v)CcS&O^Iihc58U69P=pKbk{J
z2n>`VOUOiRqMM*X&T1Gd)Uq;U$t2_nn-{W+yjYlL^AIY+gGJ%7-L>0amp{Kd_~X~d
z)4Q*`uSf540kL|3*a^jRocOZ+HL(Bf?~_@Wp2~owjAid^E<?a1DfL({hLNJ19iw<^
zck5VGp1IQMScQrr#Ok~R4RjZbh}7k>l!d5g7H3w7qMMd@Qk1fqG>}b<xR5@*g3A?Z
zm>rX-EK=sV9!pE;^eynXFHbtPJJ^fbbd|l1RY{lU(!3-El2TWsDIqC~5wKvCYs0;l
z&s~|HR3e;JqChk1y9DHOeYpySi4i`z?zh-}RmN>Lq+8r(!R9O5Y_OUZKF|yW+}A8j
zyI#K|&?yjCgaA`SqNrJzbbC|AK_+Sw-2^{!hCeIRvI+j@+w`mOhaKX|0$`l&0=Rfp
z2(z-VO6IPK9#Pr#dPL>awJSn^Df%W0L`An5WgKFnc6IsSF;%MywQ7Rs`S$!eMEO-j
zd4?!ohu7kVv#sE2l$-Yu>G=9#6W*9p(SAE{{+kb+KXTrGdjb5>7r^OxKR-&wZhq#T
zdm{a=oOy@RNH^6z=U5sTS*d%x`#3w9F5sl+pSC;KMO`0?f6k&Z&Aes)e=hT97T>q*
z|KaTaf#Ul=^5*(>Y5R6*`(Ku|b1rQs*R=8F|L!;6(7x@GzuPXkdfO#`?|i$y1phy~
zWcML8y8nuDV79w&=}Pl;G5iwWCE$CW@W6fdg<82iZR&7sk}4*qv0}m_Rm^d+`vw+1
zrlZJ@Wg?ZuH?Xe2u0U+8z)2n%<#mE62%<?4NrK2FLBF9;-=z8A;V{uHJ`8R9X0oTh
z<L<|%`b%ZNe|ab9RPtK%5ipKi4uotzw)%L1{`)#zctP`eKwRfffpM7^9wTEnI>l3f
zi!g!1_3w7KJ^eLcc>h$ZaxG?04U2%o#q01_7ahs!U9fwR^CVA7?O;s`>$Bmjs$ZHL
zqvnEH9|yAl2z{HL7?2H%4-LqnLiUTpISP444Y~tuk49*Bd5_XlkENv_N$b}eg`=JX
z(#5HB%U&4I0Lt2>!39pL!$~H!tNTxXsbydoV1!h&52ktat6Hbwp-%P2ehgfoKU@)~
z36k-B3>VsqL41b@?Vc<bL1RBk2xVbZ-4XLrEbq+hW<@z0l48H}pSmwZfkKuP5JdjV
z)9Ii0@h_GZ3n{Tsw&6-*qIrvy_qG*^NsevHm|2nvS7@P4E0r_EVD6D_khj_}?WB|q
zv&Ok4t0<5$%82t8+15GhH6`3K)M%p`FI!9LlCX;KiUTQfUSi1!uyf~BBZUxFw7BsI
z8O2y6rIFMLf}B*85+WRGok2=r?ZF;OkjHK*D-j7LB??>-jQd8lnlywu?U7SX3C9`+
zgenqh@0Au!Z~`G=6mOg*Mqxsgw_I}|Bq&l+%B5_DHQF-PPywzBN33ZyqR2N0D6y`v
zsxUM}g?WWpg=vKWH(X&<>13Hhjxp^qc&2fS!0DE?!YhxML5>E6I8s{29mPTzA(&=H
zDlIK?$TLn`Zb_shkrMc{0fE*Sr?C`LI&C>~k}5?wX$NnyrERN0k!di}ywPAj#f)<<
z02wPrZ#AcyThlV5s3t->MVW$gh~?OWgmyI37$u~oMk2!+rG%Ce?Bf=e85@rvZgfRd
zMSvl#jb@%Tt+NdnKw56B^n@dfY*<D(HY_QwD9RY5@VqgeT8fb~8dlXe9th!7L?Be;
zlG2Kjj6pdolx(pRSV-X-2y6-w!XQ{E!-y^^uPDnHU=c84$|CKIlG1Z*xR=@z$05EU
h1R1Lstr)2ot{AGQuBfW0tf<JO{0sVP>qP!1008S<14jS=