Skip to content

Commit

Permalink
update proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@belolourenco
belolourenco committed Apr 5, 2024
1 parent 38f061a commit df89a2e
Show file tree
Hide file tree
Showing 10 changed files with 100 additions and 88 deletions.
2 changes: 1 addition & 1 deletion examples/distributedLockNetwork/LDTDupl/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@
<proof prover="7" timelimit="1"><result status="valid" time="0.77" steps="6255"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.5" expl="postcondition" proved="true">
<proof prover="7" timelimit="5"><result status="valid" time="2.68" steps="42422"/></proof>
<proof prover="5" timelimit="10" memlimit="1000"><result status="valid" time="1.22" steps="158463"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.6" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="1.15" steps="84540"/></proof>
Expand Down
2 changes: 1 addition & 1 deletion examples/leaderElection/ChangRoberts/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@
<goal name="act&#39;vc.0.9.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="act&#39;vc.0.9.0.0" expl="postcondition" proved="true">
<proof prover="3" memlimit="2000"><result status="valid" time="1.51" steps="125186"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="13.78" steps="904149"/></proof>
</goal>
</transf>
</goal>
Expand Down
132 changes: 66 additions & 66 deletions examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified examples/mutualExclusionConcurrent/BakeryAtomic/why3shapes.gz
View file
Binary file not shown.
34 changes: 17 additions & 17 deletions examples/mutualExclusionConcurrent/Peterson/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,34 +9,34 @@
<path name=".."/><path name="Peterson.mlw"/>
<theory name="Peterson" proved="true">
<goal name="eq&#39;vc" expl="VC for eq" proved="true">
<proof prover="1"><result status="valid" time="0.000000" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="refn&#39;vc" expl="VC for refn" proved="true">
<proof prover="1"><result status="valid" time="0.000000" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
<goal name="a1&#39;vc" expl="VC for a1" proved="true">
<proof prover="0"><result status="valid" time="0.080000" steps="16549"/></proof>
<proof prover="0"><result status="valid" time="0.08" steps="16549"/></proof>
</goal>
<goal name="a2&#39;vc" expl="VC for a2" proved="true">
<proof prover="0"><result status="valid" time="0.180000" steps="20859"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="20859"/></proof>
</goal>
<goal name="a3&#39;vc" expl="VC for a3" proved="true">
<transf name="split_vc" proved="true" >
<goal name="a3&#39;vc.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.060000" steps="1201"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="1309"/></proof>
</goal>
<goal name="a3&#39;vc.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="a3&#39;vc.1.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.030000" steps="9473"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="9522"/></proof>
</goal>
<goal name="a3&#39;vc.1.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="a3&#39;vc.1.1.0" expl="postcondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="1.394695" steps="198668"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="1.39" steps="198668"/></proof>
</goal>
<goal name="a3&#39;vc.1.1.1" expl="postcondition" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="2.330000" steps="316869"/></proof>
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="2.33" steps="316869"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -47,33 +47,33 @@
<goal name="cs&#39;vc" expl="VC for cs" proved="true">
<transf name="split_vc" proved="true" >
<goal name="cs&#39;vc.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="104"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="104"/></proof>
</goal>
<goal name="cs&#39;vc.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.870000" steps="94238"/></proof>
<proof prover="0"><result status="valid" time="0.87" steps="94238"/></proof>
</goal>
</transf>
</goal>
<goal name="a4&#39;vc" expl="VC for a4" proved="true">
<proof prover="0"><result status="valid" time="0.100000" steps="19657"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="19657"/></proof>
</goal>
<goal name="initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="78"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="78"/></proof>
</goal>
<goal name="stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
<proof prover="1"><result status="valid" time="0.030000" steps="55"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="55"/></proof>
</goal>
<goal name="stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
<proof prover="1"><result status="valid" time="0.020000" steps="235"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="235"/></proof>
</goal>
<goal name="safety" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="84"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="84"/></proof>
</goal>
<goal name="safetyA" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="71"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="71"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified examples/mutualExclusionConcurrent/Peterson/why3shapes.gz
View file
Binary file not shown.
14 changes: 13 additions & 1 deletion examples/paxosNoRefinement/paxos/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,19 @@
<proof prover="3"><result status="valid" time="2.24" steps="13755"/></proof>
</goal>
<goal name="max_p" proved="true">
<proof prover="2"><result status="valid" time="1.14" steps="128850"/></proof>
<transf name="split_vc" proved="true" >
<goal name="max_p.0" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="max_p.0.0" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="max_p.0.0.0" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.43" steps="80380"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="propose&#39;vc" expl="VC for propose" proved="true">
<transf name="unfold" proved="true" arg1="indpred">
Expand Down
Binary file modified examples/paxosNoRefinement/paxos/why3shapes.gz
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion examples/waitFreeRegister/fourSlots/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="a&#39;vc.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.89" steps="18454"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="1.11" steps="18463"/></proof>
</goal>
<goal name="a&#39;vc.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.41" steps="72900"/></proof>
Expand Down
2 changes: 1 addition & 1 deletion test.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,4 +73,4 @@ echo "Failed: $failed" >> $GITHUB_STEP_SUMMARY

echo ""
echo "Replayed $runned from which $failed failed."
exit $failed
exit $failed

0 comments on commit df89a2e

Please sign in to comment.