From f0dab2a5d5f3a2a086852b66633335a5960fd03f Mon Sep 17 00:00:00 2001 From: Jorge Sousa Pinto Date: Wed, 17 Apr 2024 11:14:06 +0100 Subject: [PATCH] fixed some obsolete proof sessions --- .../mutualExclusionToken/selfstab-ring.mlw | 17 ++--- .../selfstab-ring/why3session.xml | 60 +++++++----------- .../selfstab-ring/why3shapes.gz | Bin 2057 -> 1358 bytes 3 files changed, 29 insertions(+), 48 deletions(-) diff --git a/examples/mutualExclusionToken/selfstab-ring.mlw b/examples/mutualExclusionToken/selfstab-ring.mlw index 85598f4..6432011 100644 --- a/examples/mutualExclusionToken/selfstab-ring.mlw +++ b/examples/mutualExclusionToken/selfstab-ring.mlw @@ -33,24 +33,17 @@ module SelfStab_Ring let rec lemma first_last_fl (w:world) (n:int) - requires { n<=n_nodes } - ensures { n>=0 -> (forall j :int. 0 w.ring[j] = w.ring[j-1]) -> - w.ring[0] = w.ring[n] } + requires { 0 w.ring[j] = w.ring[j-1] } + ensures { w.ring[0] = w.ring[n-1] } variant { n } - = if n>0 then first_last_fl w (n-1) + = if n>1 then first_last_fl w (n-1) else () - - (* crucial lemma to achieve an unbounded proof *) - (* of the atLeastOneTokenLm lemma *) - (* lemma first_last : forall n: int, lS :map node state. *) - (* n >= 0 -> *) - (* (forall j :int. 0 lS j = lS (j-1)) -> *) - (* lS 0 = lS n *) - (* lemma atLeastOneTokenLm : forall w :world. atLeastOneToken (refn w) n_nodes *) + predicate inv (w:world) = forall n :int. validNd n -> 0 <= w.ring[n] < k_states /\ diff --git a/examples/mutualExclusionToken/selfstab-ring/why3session.xml b/examples/mutualExclusionToken/selfstab-ring/why3session.xml index c8f5d85..3417bb5 100644 --- a/examples/mutualExclusionToken/selfstab-ring/why3session.xml +++ b/examples/mutualExclusionToken/selfstab-ring/why3session.xml @@ -2,8 +2,9 @@ - + + @@ -14,55 +15,42 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + - + - + - + - + - + diff --git a/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz b/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz index 949c9cdc8956d3b862867f2e2f134088942d51d4..922a484fb1aa216b04a8641865b4a95b2cfb506d 100644 GIT binary patch literal 1358 zcmV-U1+n@ciwFP!00000|CLs4Yuq>x{=UD$-*VSdkVfxEafP@PcjpUW0d>jKai<1TAm%cZ+)(7eL;RV{m=#hRV9L}lp1 zEpp0^b6rR`Teos|$LKyE9%C`BOCD45n3Bh|97thG9y-l~g+A>Mcj4mxYfXky)An#Y z-P}2Rq`O?QJ8XCVwncWUUd!OBVdR368~WU^TF>QPE!^qgcE_8z^LN2Lx!c7S8Sl5> z)AoDy_dgehcznD&T|Dj{k1?Q{+)12@d!lZi*E!)C=&5b@c9$7GocY?Az5C#9aWol( z1AQ$=>va2;?G-_^bMI+U1oM*Uk2LjRdq7!TcUp0`4Ow8wH}_OtC2H}oKc1TXE^JSD z$j6>_55~|jRW=-A+I6tf@M3u?Nv`_WeACXk=32h^!PIhV&Nznl&iLks@>Uh=^RkC_ zT>eTs-1~eq79Zd4$?Z@{siE7yesq5(@%mitP{r{SAGW*D<3~iF&Ug!A8c~b#qO?cj zvh%blYOx$So~6~I=6E0S@;UPt(tZ@z4&{}Y{G$DKgUit^WH$KcYF6`FZEA-1>!wzi zrdHWV8QM1aRqonnXM1pJ$agqt61251#otB8Eh)5J4e=Iil$` zd{xRGU23@#qvF_b#kQDyDB49XcR+O)DVnzZvWV-yn%;IUW||q}SLKE%DMT&1j-M-( ztKoDOsKOtscGaB{+?R3cm*Z4ZHiVwD;ZG2m(6xs5_$cQJH!oPtlr=}J&JJ~Vgu5h^ z))YQX6SuY=ydF;7n7D?5FKcFkyS0mQJv1I zgsiFiTwXd}74Ww6`9#jCyB^f#rj#oJ7kGT~0C0iEDgRH{CmosW_@E%e`_|-j*Av;j z#q;$wn7Xlc+Gt7EwQSz`QsJA9al6Kwsq$&tc;7ZwvM+Bw|Am`2=()4_IXAb?-^C?v zivw@0sqX7G5{0N9phtn%xa~fToTBTCDQ_TS3e)ae27@8bxjQhO&;sp*c3zlz^H;Oq z#n1b%an~W(6oDrz-anlFyJ`P5Uo1q_jY|%66Sz-;7)?aeG!iYsgg`2=)RINwl!ySy zB%V?rim^s%?NZdrByXVNmLbe@qNr8?Q9C3;>P9E2H3jAcuv9T(!B~M%k(7+W2~V9D zim2pMk{*0CR5M_qqQn}jt+KMkL!*f&hIy?71#Os)Ll&8Q6la7)oJPEN;p>aY0*M?V|T2AI7wFVLx0G`7n zK{@874iVe0qZd)8iZjb$E>d|DIKw)%7KCU{T$F)gx`LKq#@?SgtKsmP^Zp Q<$R9re*h_>Ucn9k00~2}3jhEB literal 2057 zcmV+k2=@0MiwFP!00000|Ls~^izB-ce)q5N+eywLAXVuab`EP6OdHG|2utU2PHfZ)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~bVhOmfPP5oRXg;{=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`cZ$ zY6$9Ccf78LMw~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_2kvmlathwKjfi5GgMQQG`U_ zdSGCI3r@ks0bJCX8cJXe?lmPO6f3*{7Zpv+`ih#FO?I#KAZhs}s9%R8MQxabC?!)L^2ukV-;byjp0K_9tmik{XUqqy!#OOg_A3_tx zIVLJU<*8$hQyJFm8&Ae^$SyCQd-&|aG+a}n^t=q47{Z3h`s)7E-_je#dJLu;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+kl;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)-e_s8vC3+v0Towf38n&lNfO$=mn~f|D76SRpa^-_ n^~`rx2#Vhlb%m-zSs^7kRtOdH3RwmAlDhu_l