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

---
 .../selfstab-ring/why3session.xml             |  45 +++++++++++-------
 .../selfstab-ring/why3shapes.gz               | Bin 1366 -> 2072 bytes
 2 files changed, 29 insertions(+), 16 deletions(-)

diff --git a/examples/mutualExclusionToken/selfstab-ring/why3session.xml b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
index 79299a0..0eab7b2 100644
--- a/examples/mutualExclusionToken/selfstab-ring/why3session.xml
+++ b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
@@ -14,26 +14,39 @@
  <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="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>
+ <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.2.1" expl="postcondition" proved="true">
-   <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="2.140096" steps="21941721"/></proof>
+   <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>
   </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">
diff --git a/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz b/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz
index af6e291cc95f37a38e0e2618fba02986afa22e73..6249c67caa00446de09ef2d23685386e35bc24da 100644
GIT binary patch
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

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`