From 7301ce7b377cf0de8d0a9cb932481b0a0b39ca7d Mon Sep 17 00:00:00 2001
From: Jorge Sousa Pinto <jsp@di.uminho.pt>
Date: Fri, 12 Apr 2024 17:35:48 +0100
Subject: [PATCH] updated selfstab-ring proofs

---
 .../selfstab-ring/why3session.xml             |  58 ++++++++----------
 .../selfstab-ring/why3shapes.gz               | Bin 2072 -> 1253 bytes
 2 files changed, 25 insertions(+), 33 deletions(-)

diff --git a/examples/mutualExclusionToken/selfstab-ring/why3session.xml b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
index 0eab7b2..8293788 100644
--- a/examples/mutualExclusionToken/selfstab-ring/why3session.xml
+++ b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
@@ -2,7 +2,7 @@
 <!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="1" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Z3" version="4.11.2" timelimit="1200" 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"/>
@@ -14,38 +14,30 @@
  <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" timelimit="1200"><result status="valid" time="0.754841" steps="32013"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.1" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="1200"><result status="valid" time="0.006626" steps="7"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.2" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.108042" steps="958375"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.3" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="1"><result status="valid" time="0.141224" steps="5729"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.4" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.019330" steps="79453"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.5" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.031172" steps="153247"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.6" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
-    <goal name="trans&#39;vc.0.6.0" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.705729" steps="9210314"/></proof>
-    </goal>
-   </transf>
-   </goal>
-   <goal name="trans&#39;vc.0.7" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.018245" steps="62654"/></proof>
-   </goal>
-  </transf>
+ <transf name="split_all_full" proved="true" >
+  <goal name="trans&#39;vc.0" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.015921" steps="54048"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.1" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.013354" steps="39489"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.2" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.170432" steps="1539135"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.3" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.013887" steps="42157"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.4" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.017414" steps="79357"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.5" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.030093" steps="153051"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.6" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.306929" steps="3138168"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.7" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.015670" steps="62268"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz b/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz
index 6249c67caa00446de09ef2d23685386e35bc24da..b4b09f1dee50b91475b467650cfdb96be9ac7b18 100644
GIT binary patch
literal 1253
zcmV<B1RDDviwFP!00000|K(R(Ya2%te%G(iTiS%coHO?l2ZX__K{Qap_EF5W5pg6V
zsVV*UJ+m__X>FO*CA1+0dv`A1`ObGPGpv4iIp2S9_h~=>oOb*5cJtF*&0qdFb8p;c
zwb{nBcOO^#gFB@C?67p7wz0<^j)TR|?y85tmOU=rtDXhg8u2%?{(7FbyZL$(c4_9W
z9PKlD^l&>&dO;8Ox)*^K-dy#9_}rU7>o>RV?ZA7xKAhRfW~Zy2Zg#qt)lOGCS@g&y
zAs~QzTX+@)XU33d)|<iE6<NWuHw}DS(aW{Fad-RV-tT@-b!l(}Bf--BvEALp7oR@%
z>=<TV@Aik)oufy-E8)7`dh^?$y^U(%;{?YM`NkFsjw!%X3MQU!W^TRt+ylYOTP|sM
zrp7Mm&-I*gsh2$`ca*Fl|2?Q>`7fKmX>VCx?)69<$T5{5u$yW0!`iJo?A&I*N*jL{
zd)bRKm;7dSzuh0gb`#eJYM>JNF69jgt5$U;D-Y3~`)pC%euF_h83y%v?bs(m`A)*$
zAJYAL6Px@orgvxI)txWK{Xfaqvn4$cQIa%Vr(d~UziJx)CC%SN%Y5ZnzpwN3-zI1A
z50mq>-P6fgJS#ct!?M?lr&4s<toIR?4<}adBVD0-av!yfE{L{(u=3%FuMu$~;*|(1
z5ndvCer4LX&44NAbr_UzkEr$)Lrd#%SjAOor?rP-rk=^ZUZTx~?A5V5rwY~a;%HD!
zUv|T&bqURDInCp8>M0vRAF|mV*o1CactwxeS2TIVYNxEl;$c&_7H&=edcb#6$HUqP
zJ{`$(;sH|AL?cl^>%*_55UYEdPs{s^y<;(nm7jgLH_+lmQ8hcaYC5M9il%m49&bD;
z;LDq*j=ZGq`lzlXrCt#<p!O*RpaCsT`TxfHBqNiVI4UUcF*Rk}a-!N>p02OsQY&lI
z2Gv<h+2zg03ct8<p04xBRQWV*VoV#a-WRL)ztChbI%SrQbNJx=U0Tp|{N~Y9-PeO9
z3DG0KoEcuzv>lD&qUFWbH?ngIJIn_LOC~4Z4Ga@ngeJ7@;&iv1n(ZdN-+oM+hTu~K
zbyoUxfB17X{2rdoWHP~JhbBbfvt-sV8A4FBB5jOpjvaJtmK`@D8ZEpFig~F5CW%3K
zlayc*=Az>SLobciHkiy%`3PD{?UPE}Sk!^x98?FglLU3vIEH~Ujv*<X63bkpbc7Ni
zTRYdC8i3wMCb$j)ydYsVXDJPrCTL(hFit=-0FyE{=p<05s3TJn1+c`Tw@gM5ihy<i
znjC^qq*DfwycNnhEl7&>7_<_RfWQW%lmL<gaDs>+C>jaLMPboNDPk^27?9a1Wu4(R
zTA@YOfWk9nw3iwLh!PIqfMh9J&W%n|0C!er8<Gx~IeG&=iGt)688c*MfXVEobSg^Y
zBN{=XwX`f0q!^IGFqeFg$pOn=XUu^jN?9evnbUlZyhH2|I%FN#4onBST4sYtwG0-7
zhh(`mWrYisAR?6kWryODWn>%-AP`n~#jJDENzT19nsVvo9Ce54lBLly3eeny#8jYI
zj5StS?KE-)%FNMrXf9b|py~&Z&MGD`Vor|AkxNR2u*}c7>A3E=>bUGU^(5~&b{sm+
PF46r3y|^dS7ZLyf{0eHR

literal 2072
zcmV+z2<P`7iwFP!00000|Ls~^ZyPrje%G(iTXq{1;Qg|Q3kU&(F(9PCBA9(NI2_Je
zh$9)261V?;4=*!AjwEN?U|X~`kXS?VTtA-g3~BivKP->;=FuIOU)|xj-S7Uj6w4p}
zxiIg{?ryhl-O+ryJD$wR9T%sK`MhsyQsd!a^}*cK*rH8MHs)=OEG+f%>qY&3+3gR@
z?am(D!rT~GNARP@w_#8-_+fsmnT3gWH#Gx$=ADK4^{x3S*uCAJGCiL3WYm*MPu4u@
z$*9MDJbVKZ*kbdOx3ltcs!s_<wF=H|Knrhbm4t7j^k!?;=Hckf$HNyFr-CEg8`zkq
z{o$c~^Z8SahBUkF;dr`xFz};$@adYvcK6>9dwPnA_XE;Dfp3yhAw2|SgrM-eUVJe3
z=6HA7e{#DT;~GQmz0EKjo_$I^v@jh<ea?I}+Yab~4L_5?hhek$`u0Pi!=}EYWTxj`
zv-O#8QTi6cb4cG$lqSUbHd7b?_I`WG;5@TQhq{aq<V&~at9jVAA6j_!IgP>b8tXAO
zKk6TShN?$br%{itUd=NCN+Ca8Knta*b7;NT#BG$DprY0jw*=*GNuM*1sKU6=Cn!Ue
z4+!zgm_ktUGNgVbLsYIefO5tdy@7wGroeZ(sR4Xoun9e)CT!#X`$Yn@q#OTH`iC}Q
z(Yj=4n7cKngV`PL+^%_OAqbYar0d1w{&=$cUAsL&lk@C6xXu?})QTe>?SQ%5=d>Vr
zv6npGnVEFEZe$+U_((PW0;chTXnf=upFy)Z1#yLA{8@^52I`Xky67V_S@x`*c|;3x
zQ{Qu_28ub?!f?{Vo@Lw29(ILrVX0u;q+|&#`T)&phYW8Xnnnp-(3xihltO+qhn5hS
zC`*=*iQ6bQL4}<4Fjlx_Wyz9B$rCoOWUn^>IK@O3zczvYa})TU9{l=J{@$1Jv<K((
z4#T_;&g~M<+L_lVg51>ioL1o#S?PN`kDhgl1sv1e<964ks_RSf=d3E@$}97KKjzPD
zzOU^6ZuWmi^ZkpQCSEVnuNUb*8EfZUq$gKr-%rCY>3-X-IbStT=6>P9ytl}opSQbi
z`^)mjHwSn8@^E_dW%uRiTFCL<;&8l%6eep=VF5CQrzDu+Y@%>I@@JSShS_fnc}g%=
zOF_lC*6P5?f|9Jx2|37J2qH+An_rT$R~Bbch+-HEX~NEooP*dThzkYPJGji#VRbC5
zlBwpY9y#U*{S#!|(^SXj1be~JtLk+iXu(fa=j`+%rLQ1ULQ*mlR4~fD;Xcc!)bA$D
z#2GWa%;@hDkWckxV)}&<KDq8Mll`uYFH}#N@Ir-{ue?xw)U?QfW+>qPg^Fn!^_`JU
zfw*D>lmZgP3l)>ppfe3JaU10(_>nXGS>cvV@IQZLy$FAJ4_(;+jI+*&i{Fa-RarzO
z^VCF-s7#|CQ8`WRiV;u>xyb@ikuFu4hM2frU48>k-KxT^njm`qu6h}w{3@b6LzJ)m
zH$X+vK40bLZS4E6x2iwtR<(M)RsGTDv+G;%_qkQ2FGEB6FK7pFn*18iYA>tdZ|PkE
zzSr>|xF3GwY`r~gYX3fnCu~f^2^&7*IdEJ|-(&eN#8J@4GK$LLd#rRIUxC?hVvqL7
zXfGL}V2DOTBpM=@4E=_K{Y_l=84e3+^I>Y+KgM`sG~?XVf9VYL!2zI}T<}^Xkf%Y3
z@$3{uB^>y|Qz{G?#~oDXJ19$QAUd_C{Q)pH7bf1qk621DIJ2rtt6pP0spC|&$%()C
zlAlY*VXhax9SSWs97G~a@fQQz-S+e!zY%wjFfMoW1#81*`ulkHCm2a+^~OiF$hA_O
zWe7N&>_Xt@3s(d9_TpHCm!f+=MCU<?T>*#lmfwJI$l|5_8S@1q#fS|Nc<~+@|C}%p
z>64EgYnV#gnqtGzS%U2H;(3JMT*%?d2W8|XY^;ZkM(?Y;kN<{2P#Td1I@^2GJh)Xn
z?S*({8Tb338BVrIKxK;W{fl@pxJbC@_(@Q1LWgm%ph0EyorG~=mf#d<S|#PGXU%@+
zKBoJ%m!PEtRF?bvc>47&{Atr-!JV?EGep^zH62G<A#SY|FvE4*q9v(tg%+KminU6z
z##n(GE-Z1JSk@>f7~*)zDhgtx;YvzvRfmXZS}Zx2jT4S4O{7I+NoYk_#X;0KLtJYW
zWgVuf5mM{cVu>5ZX(KHSq9lk~grt>18SI!8gsE0rL#br6C7r~0DJu~KsWV**%gjj4
znRAXKEE`L>;8t5oK~M!j)-cvOB{jsagkzAFp{>ybA<Z~<AgF_&>sm@kYY>N2Ig+%a
zmbS=p;RtWJ1wo90B!}EBYa82iq-{_`8)YDUg^6agL#>y@G0KimsR`v+bQp82Efa_f
z=A^_H6o)9aA+o_zHci8fgG5~mu{w)MLxe(Th!Pf@Y9LZ0TLG9@!wG{xd1H+s)<;Qj
zMNoxxg;j+i6j5PbVOC*U;fS(sA&f>Vqhup2VjRm3{7cbVA&Ajqs!So{8q1x*sB1u~
zvyu_l2`4Brk}fH(D5{9Ah^h$q78T)9vr~jX<yehbgPo>Y`5DTD!!6NzNohsNCCwI5
z3|L~2WsN{^dgg{x+Ca3#(uOZ7uPD2usU&Y1mQ-1Xgl!~OT4|xBk%S5?)RM}Iic6Zr
zb{)5HH`1^_1aNgwv~7o6s~OX%Su#;EUNKfNS}{^FTrpHpT~T$(-2VVPFNt$dC;$La
CnhCf7