Skip to content

Commit 5fd9364

Browse files
belolourencobelolourenco
committed
update proofs
1 parent 83eba15 commit 5fd9364

File tree

10 files changed

+100
-88
lines changed

10 files changed

+100
-88
lines changed

‎examples/distributedLockNetwork/LDTDupl/why3session.xml

+1-1
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,7 @@
126126
<proof prover="7" timelimit="1"><result status="valid" time="0.77" steps="6255"/></proof>
127127
</goal>
128128
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.5" expl="postcondition" proved="true">
129-
<proof prover="7" timelimit="5"><result status="valid" time="2.68" steps="42422"/></proof>
129+
<proof prover="5" timelimit="10" memlimit="1000"><result status="valid" time="1.22" steps="158463"/></proof>
130130
</goal>
131131
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.6" expl="postcondition" proved="true">
132132
<proof prover="5"><result status="valid" time="1.15" steps="84540"/></proof>

‎examples/leaderElection/ChangRoberts/why3session.xml

+1-1
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@
5656
<goal name="act&#39;vc.0.9.0" expl="postcondition" proved="true">
5757
<transf name="split_vc" proved="true" >
5858
<goal name="act&#39;vc.0.9.0.0" expl="postcondition" proved="true">
59-
<proof prover="3" memlimit="2000"><result status="valid" time="1.51" steps="125186"/></proof>
59+
<proof prover="3" timelimit="20"><result status="valid" time="13.78" steps="904149"/></proof>
6060
</goal>
6161
</transf>
6262
</goal>

‎examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml

+66-66
Large diffs are not rendered by default.

‎examples/mutualExclusionConcurrent/BakeryAtomic/why3shapes.gz

-4 Bytes
Binary file not shown.

‎examples/mutualExclusionConcurrent/Peterson/why3session.xml

+17-17
Original file line numberDiff line numberDiff line change
@@ -9,34 +9,34 @@
99
<path name=".."/><path name="Peterson.mlw"/>
1010
<theory name="Peterson" proved="true">
1111
<goal name="eq&#39;vc" expl="VC for eq" proved="true">
12-
<proof prover="1"><result status="valid" time="0.000000" steps="6"/></proof>
12+
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
1313
</goal>
1414
<goal name="refn&#39;vc" expl="VC for refn" proved="true">
15-
<proof prover="1"><result status="valid" time="0.000000" steps="0"/></proof>
15+
<proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
1616
</goal>
1717
<goal name="a1&#39;vc" expl="VC for a1" proved="true">
18-
<proof prover="0"><result status="valid" time="0.080000" steps="16549"/></proof>
18+
<proof prover="0"><result status="valid" time="0.08" steps="16549"/></proof>
1919
</goal>
2020
<goal name="a2&#39;vc" expl="VC for a2" proved="true">
21-
<proof prover="0"><result status="valid" time="0.180000" steps="20859"/></proof>
21+
<proof prover="0"><result status="valid" time="0.18" steps="20859"/></proof>
2222
</goal>
2323
<goal name="a3&#39;vc" expl="VC for a3" proved="true">
2424
<transf name="split_vc" proved="true" >
2525
<goal name="a3&#39;vc.0" expl="postcondition" proved="true">
26-
<proof prover="1"><result status="valid" time="0.060000" steps="1201"/></proof>
26+
<proof prover="1"><result status="valid" time="0.06" steps="1309"/></proof>
2727
</goal>
2828
<goal name="a3&#39;vc.1" expl="postcondition" proved="true">
2929
<transf name="split_vc" proved="true" >
3030
<goal name="a3&#39;vc.1.0" expl="postcondition" proved="true">
31-
<proof prover="2"><result status="valid" time="0.030000" steps="9473"/></proof>
31+
<proof prover="2"><result status="valid" time="0.03" steps="9522"/></proof>
3232
</goal>
3333
<goal name="a3&#39;vc.1.1" expl="postcondition" proved="true">
3434
<transf name="split_vc" proved="true" >
3535
<goal name="a3&#39;vc.1.1.0" expl="postcondition" proved="true">
36-
<proof prover="0" timelimit="5"><result status="valid" time="1.394695" steps="198668"/></proof>
36+
<proof prover="0" timelimit="5"><result status="valid" time="1.39" steps="198668"/></proof>
3737
</goal>
3838
<goal name="a3&#39;vc.1.1.1" expl="postcondition" proved="true">
39-
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="2.330000" steps="316869"/></proof>
39+
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="2.33" steps="316869"/></proof>
4040
</goal>
4141
</transf>
4242
</goal>
@@ -47,33 +47,33 @@
4747
<goal name="cs&#39;vc" expl="VC for cs" proved="true">
4848
<transf name="split_vc" proved="true" >
4949
<goal name="cs&#39;vc.0" expl="postcondition" proved="true">
50-
<proof prover="1"><result status="valid" time="0.010000" steps="104"/></proof>
50+
<proof prover="1"><result status="valid" time="0.01" steps="104"/></proof>
5151
</goal>
5252
<goal name="cs&#39;vc.1" expl="postcondition" proved="true">
53-
<proof prover="0"><result status="valid" time="0.870000" steps="94238"/></proof>
53+
<proof prover="0"><result status="valid" time="0.87" steps="94238"/></proof>
5454
</goal>
5555
</transf>
5656
</goal>
5757
<goal name="a4&#39;vc" expl="VC for a4" proved="true">
58-
<proof prover="0"><result status="valid" time="0.100000" steps="19657"/></proof>
58+
<proof prover="0"><result status="valid" time="0.10" steps="19657"/></proof>
5959
</goal>
6060
<goal name="initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
61-
<proof prover="1"><result status="valid" time="0.010000" steps="16"/></proof>
61+
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
6262
</goal>
6363
<goal name="initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
64-
<proof prover="1"><result status="valid" time="0.010000" steps="78"/></proof>
64+
<proof prover="1"><result status="valid" time="0.01" steps="78"/></proof>
6565
</goal>
6666
<goal name="stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
67-
<proof prover="1"><result status="valid" time="0.030000" steps="55"/></proof>
67+
<proof prover="1"><result status="valid" time="0.03" steps="55"/></proof>
6868
</goal>
6969
<goal name="stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
70-
<proof prover="1"><result status="valid" time="0.020000" steps="235"/></proof>
70+
<proof prover="1"><result status="valid" time="0.02" steps="235"/></proof>
7171
</goal>
7272
<goal name="safety" proved="true">
73-
<proof prover="1"><result status="valid" time="0.010000" steps="84"/></proof>
73+
<proof prover="1"><result status="valid" time="0.01" steps="84"/></proof>
7474
</goal>
7575
<goal name="safetyA" proved="true">
76-
<proof prover="1"><result status="valid" time="0.010000" steps="71"/></proof>
76+
<proof prover="1"><result status="valid" time="0.01" steps="71"/></proof>
7777
</goal>
7878
</theory>
7979
</file>

‎examples/mutualExclusionConcurrent/Peterson/why3shapes.gz

1 Byte
Binary file not shown.

‎examples/paxosNoRefinement/paxos/why3session.xml

+13-1
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,19 @@
3434
<proof prover="3"><result status="valid" time="2.24" steps="13755"/></proof>
3535
</goal>
3636
<goal name="max_p" proved="true">
37-
<proof prover="2"><result status="valid" time="1.14" steps="128850"/></proof>
37+
<transf name="split_vc" proved="true" >
38+
<goal name="max_p.0" proved="true">
39+
<transf name="inline_goal" proved="true" >
40+
<goal name="max_p.0.0" proved="true">
41+
<transf name="split_all_full" proved="true" >
42+
<goal name="max_p.0.0.0" proved="true">
43+
<proof prover="2" timelimit="1"><result status="valid" time="0.43" steps="80380"/></proof>
44+
</goal>
45+
</transf>
46+
</goal>
47+
</transf>
48+
</goal>
49+
</transf>
3850
</goal>
3951
<goal name="propose&#39;vc" expl="VC for propose" proved="true">
4052
<transf name="unfold" proved="true" arg1="indpred">

‎examples/paxosNoRefinement/paxos/why3shapes.gz

235 Bytes
Binary file not shown.

‎examples/waitFreeRegister/fourSlots/why3session.xml

+1-1
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@
8181
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
8282
</goal>
8383
<goal name="a&#39;vc.1" expl="postcondition" proved="true">
84-
<proof prover="2"><result status="valid" time="0.89" steps="18454"/></proof>
84+
<proof prover="2" timelimit="10"><result status="valid" time="1.11" steps="18463"/></proof>
8585
</goal>
8686
<goal name="a&#39;vc.2" expl="postcondition" proved="true">
8787
<proof prover="0"><result status="valid" time="0.41" steps="72900"/></proof>

‎test.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -73,4 +73,4 @@ echo "Failed: $failed" >> $GITHUB_STEP_SUMMARY
7373

7474
echo ""
7575
echo "Replayed $runned from which $failed failed."
76-
exit $failed
76+
exit $failed

0 commit comments

Comments
 (0)