Skip to content

Commit

Permalink
fixed some obsolete proof sessions
Browse files Browse the repository at this point in the history
  • Loading branch information
@jspdium
jspdium committed Apr 17, 2024
1 parent 15182b9 commit fa7cdac
Show file tree
Hide file tree
Showing 63 changed files with 626 additions and 649 deletions.
56 changes: 28 additions & 28 deletions examples/changRobertsNetwork/leaderlect-ring/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -1,67 +1,67 @@
<?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="1" name="Z3" version="4.11.2" alternative="noBV" timelimit="7" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.4.2" timelimit="3" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="leaderlect-ring.mlw"/>
<theory name="LeaderElectRing" proved="true">
<goal name="next&#39;vc" expl="VC for next" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.000000" steps="2"/></proof>
</goal>
<goal name="maxId_fn&#39;vc" expl="VC for maxId_fn" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.030000"/></proof>
</goal>
<goal name="btw_next_lm" proved="true">
<proof prover="2"><result status="valid" time="0.08" steps="1849"/></proof>
<proof prover="2"><result status="valid" time="0.080000" steps="1824"/></proof>
</goal>
<goal name="initMsgs_fn&#39;vc" expl="VC for initMsgs_fn" proved="true">
<transf name="split_vc" proved="true" >
<goal name="initMsgs_fn&#39;vc.0" expl="variant decrease" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="3"><result status="valid" time="0.020000"/></proof>
</goal>
<goal name="initMsgs_fn&#39;vc.1" expl="precondition" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03"/></proof>
<proof prover="1" timelimit="3"><result status="valid" time="0.030000"/></proof>
</goal>
<goal name="initMsgs_fn&#39;vc.2" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="initMsgs_fn&#39;vc.2.0" expl="postcondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.01" steps="91"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.010000" steps="91"/></proof>
</goal>
<goal name="initMsgs_fn&#39;vc.2.1" expl="postcondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.01" steps="93"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.010000" steps="93"/></proof>
</goal>
<goal name="initMsgs_fn&#39;vc.2.2" expl="postcondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.01" steps="94"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.010000" steps="94"/></proof>
</goal>
<goal name="initMsgs_fn&#39;vc.2.3" expl="postcondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.01" steps="90"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.010000" steps="90"/></proof>
</goal>
<goal name="initMsgs_fn&#39;vc.2.4" expl="postcondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.62" steps="15361"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.620000" steps="16489"/></proof>
</goal>
<goal name="initMsgs_fn&#39;vc.2.5" expl="postcondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.11" steps="2352"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.110000" steps="2358"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="initMsgs&#39;vc" expl="VC for initMsgs" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="1"><result status="valid" time="0.050000"/></proof>
</goal>
<goal name="Steps.case_node&#39;refn&#39;vc" expl="VC for case_node&#39;refn" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.030000"/></proof>
</goal>
<goal name="Steps.case_state&#39;refn&#39;vc" expl="VC for case_state&#39;refn" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.030000"/></proof>
</goal>
<goal name="Steps.case_msg&#39;refn&#39;vc" expl="VC for case_msg&#39;refn" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.030000"/></proof>
</goal>
<goal name="Steps.indpred&#39;refn&#39;vc" expl="VC for indpred&#39;refn" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.21"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="5.211647"/></proof>
</goal>
<goal name="Steps.handleMsg&#39;refn&#39;vc" expl="VC for handleMsg&#39;refn" proved="true">
<transf name="unfold" proved="true" arg1="handleMsg">
Expand All @@ -78,34 +78,34 @@
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.0.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.0.0.0" expl="VC for handleMsg&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.27" steps="10133"/></proof>
<proof prover="2"><result status="valid" time="0.270000" steps="10154"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.0.0.1" expl="VC for handleMsg&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.30" steps="10154"/></proof>
<proof prover="2"><result status="valid" time="0.300000" steps="10183"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.0.0.2" expl="VC for handleMsg&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.30" steps="11683"/></proof>
<proof prover="2"><result status="valid" time="0.300000" steps="11664"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.0.0.3" expl="VC for handleMsg&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.26" steps="10093"/></proof>
<proof prover="2"><result status="valid" time="0.260000" steps="10105"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.0.0.4" expl="VC for handleMsg&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.46" steps="18636"/></proof>
<proof prover="2"><result status="valid" time="0.460000" steps="18663"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.26" steps="10276"/></proof>
<proof prover="2"><result status="valid" time="0.260000" steps="10263"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.30" steps="12196"/></proof>
<proof prover="2"><result status="valid" time="0.300000" steps="12197"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.3" expl="postcondition" proved="true">
<transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,get,set,(!),map,ok_NodeState,case_node,case_state,case_msg,dest1,src2,payload1,initState,initMsgs,handleMsg,inv,indpred,dest,src1,payload,localState,eq_pckt,initWorld,remove_one,s1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Mod_bound,Mod_1,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,is_nil&#39;spec,maxId_fn&#39;def,btw_next_lm,initMsgs_fn&#39;spec,initMsgs_fn&#39;def,Requires5,Requires4,Requires3,Requires2,Requires1,Requires,H4,H2">
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.3.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.09" steps="3527"/></proof>
<proof prover="2"><result status="valid" time="0.090000" steps="3501"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -116,7 +116,7 @@
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.4.0.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.4.0.0.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.27" steps="10720"/></proof>
<proof prover="2"><result status="valid" time="0.270000" steps="11322"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -127,7 +127,7 @@
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.5" expl="postcondition" proved="true">
<transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,get,is_nil,length,mem,(++),map,next,maxId_global,ok_NodeState,ok_Msg,case_node,case_state,case_msg,dest1,src2,payload1,between,initState,initMsgs,handleMsg,inv,indpred,src1,payload,inFlightMsgs,eq_pckt,initWorld,remove_one,s,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,Mod_mult,is_nil&#39;spec,Length_nonnegative,Length_nil,nth_cons_0,Append_assoc,Append_l_nil,Append_length,mem_append,mem_decomp,uniqueIds,maxId_fn&#39;spec,btw_next_lm,initMsgs_fn&#39;spec,initMsgs_fn&#39;def,remove_one&#39;spec,Requires5,Requires4,Requires3,Requires2,Requires1,Requires">
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.5.0" expl="postcondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.01" steps="223"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.010000" steps="240"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -142,7 +142,7 @@
</transf>
</goal>
<goal name="uniqueLeader" proved="true">
<proof prover="2"><result status="valid" time="0.09" steps="359"/></proof>
<proof prover="2"><result status="valid" time="0.090000" steps="361"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified examples/changRobertsNetwork/leaderlect-ring/why3shapes.gz
View file
Binary file not shown.
4 changes: 2 additions & 2 deletions examples/counter/counter/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
<?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="Alt-Ergo" version="2.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="counter.mlw"/>
<theory name="Counter" proved="true">
<goal name="trans&#39;vc" expl="VC for trans" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="0"><result status="valid" time="0.000000" steps="9"/></proof>
</goal>
</theory>
</file>
Expand Down
2 changes: 1 addition & 1 deletion examples/counter/counter/why3session.xml.bak
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
<prover id="0" name="Alt-Ergo" version="2.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="counter.mlw"/>
<theory name="Abstract" proved="true">
<theory name="Counter" proved="true">
<goal name="trans&#39;vc" expl="VC for trans" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
Expand Down
Binary file modified examples/counter/counter/why3shapes.gz
View file
Binary file not shown.
14 changes: 7 additions & 7 deletions examples/counter/counter_alt/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -1,29 +1,29 @@
<?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="Alt-Ergo" version="2.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="counter_alt.mlw"/>
<theory name="Counter" proved="true">
<goal name="count&#39;vc" expl="VC for count" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="168"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="122"/></proof>
</goal>
<goal name="count_lm&#39;vc" expl="VC for count_lm" proved="true">
<proof prover="2"><result status="valid" time="0.18" steps="46449"/></proof>
<proof prover="2"><result status="valid" time="0.180000" steps="48243"/></proof>
</goal>
<goal name="trans&#39;vc" expl="VC for trans" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="105"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="105"/></proof>
</goal>
<goal name="initWorld&#39;refn&#39;vc" expl="VC for initWorld&#39;refn" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="31"/></proof>
<proof prover="0"><result status="valid" time="0.000000" steps="31"/></proof>
</goal>
<goal name="step&#39;refn&#39;vc" expl="VC for step&#39;refn" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="23"/></proof>
<proof prover="0"><result status="valid" time="0.000000" steps="23"/></proof>
</goal>
<goal name="correctness" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="39"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="39"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified examples/counter/counter_alt/why3shapes.gz
View file
Binary file not shown.
20 changes: 10 additions & 10 deletions examples/counter/counter_lock/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -1,38 +1,38 @@
<?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="CVC5" version="1.0.3" timelimit="5" 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="counter_lock.mlw"/>
<theory name="CounterImpl" proved="true">
<goal name="refn&#39;vc" expl="VC for refn" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.000000" steps="2"/></proof>
</goal>
<goal name="initWorld&#39;vc" expl="VC for initWorld" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="58"/></proof>
<proof prover="1"><result status="valid" time="0.000000" steps="58"/></proof>
</goal>
<goal name="transSI&#39;vc" expl="VC for transSI" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="5263"/></proof>
<proof prover="0"><result status="valid" time="0.040000" steps="5229"/></proof>
</goal>
<goal name="transID&#39;vc" expl="VC for transID" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="18637"/></proof>
<proof prover="0"><result status="valid" time="0.120000" steps="18670"/></proof>
</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.00" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.000000" steps="6"/></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.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.000000" steps="2"/></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.00" steps="18"/></proof>
<proof prover="1"><result status="valid" time="0.000000" steps="18"/></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="130"/></proof>
<proof prover="1"><result status="valid" time="0.010000" steps="130"/></proof>
</goal>
<goal name="safety_by_refinement" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.000000" steps="6"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified examples/counter/counter_lock/why3shapes.gz
View file
Binary file not shown.
26 changes: 13 additions & 13 deletions examples/counter/counter_lock_alt/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
<?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="CVC5" version="1.0.3" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
Expand All @@ -10,26 +10,26 @@
<path name=".."/><path name="counter_lock_alt.mlw"/>
<theory name="CounterImpl" proved="true">
<goal name="refn&#39;vc" expl="VC for refn" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.000000" steps="4"/></proof>
</goal>
<goal name="initWorld&#39;vc" expl="VC for initWorld" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="99"/></proof>
<proof prover="2"><result status="valid" time="0.010000" steps="99"/></proof>
</goal>
<goal name="transSI&#39;vc" expl="VC for transSI" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="13479"/></proof>
<proof prover="0"><result status="valid" time="0.100000" steps="13908"/></proof>
</goal>
<goal name="transID&#39;vc" expl="VC for transID" proved="true">
<transf name="split_vc" proved="true" >
<goal name="transID&#39;vc.0" expl="postcondition" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="52"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.010000" steps="52"/></proof>
<proof prover="3"><result status="valid" time="0.020000"/></proof>
</goal>
<goal name="transID&#39;vc.1" expl="postcondition" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="transID&#39;vc.1.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="transID&#39;vc.1.0.0" expl="postcondition" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.10" steps="29231"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.100000" steps="29247"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -38,22 +38,22 @@
</transf>
</goal>
<goal name="Refinement.initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="38"/></proof>
<proof prover="2"><result status="valid" time="0.010000" steps="38"/></proof>
</goal>
<goal name="Refinement.initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.000000" steps="4"/></proof>
</goal>
<goal name="Refinement.stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="29"/></proof>
<proof prover="2"><result status="valid" time="0.000000" steps="29"/></proof>
</goal>
<goal name="Refinement.stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="155"/></proof>
<proof prover="2"><result status="valid" time="0.010000" steps="155"/></proof>
</goal>
<goal name="safety_by_refinement" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.000000" steps="8"/></proof>
</goal>
<goal name="correctness" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="23426"/></proof>
<proof prover="1"><result status="valid" time="0.050000" steps="24418"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified examples/counter/counter_lock_alt/why3shapes.gz
View file
Binary file not shown.
Loading

0 comments on commit fa7cdac

Please sign in to comment.