Skip to content

Commit a12414e

Browse files
belolourencobelolourenco
committed
changroberts: act without 2 complicated postconditions
1 parent 6088c8e commit a12414e

File tree

3 files changed

+60
-49
lines changed

3 files changed

+60
-49
lines changed

‎examples/leaderElection/ChangRoberts.mlw‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -90,9 +90,9 @@ module ChangRoberts
9090

9191
let ghost function act (w:world) (h:node) : world
9292
requires { act_enbld w h }
93-
ensures { inv w -> forall n :node. 0<=n<n_nodes -> n<>next h ->
94-
forall m :msg. mem m result.inMsgs[n] -> mem m w.inMsgs[n] }
95-
ensures { forall m :msg. mem m result.inMsgs[next h] -> mem m w.inMsgs[h] \/ mem m w.inMsgs[next h] }
93+
(* ensures { inv w -> forall n :node. 0<=n<n_nodes -> n<>next h -> *)
94+
(* forall m :msg. mem m result.inMsgs[n] -> mem m w.inMsgs[n] } *)
95+
(* ensures { forall m :msg. mem m result.inMsgs[next h] -> mem m w.inMsgs[h] \/ mem m w.inMsgs[next h] } *)
9696

9797
ensures { inv w -> inv result }
9898
ensures { inv w -> refn result = refn w

‎examples/leaderElection/ChangRoberts/why3session.xml‎

Lines changed: 57 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -2,106 +2,117 @@
22
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
33
"https://www.why3.org/why3session.dtd">
44
<why3session shape_version="6">
5+
<prover id="0" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
6+
<prover id="1" name="Eprover" version="2.6" timelimit="1" steplimit="0" memlimit="1000"/>
57
<prover id="3" name="CVC5" version="1.0.3" timelimit="5" steplimit="0" memlimit="1000"/>
6-
<prover id="4" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
8+
<prover id="4" name="Alt-Ergo" version="2.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
79
<file format="whyml" proved="true">
810
<path name=".."/><path name="ChangRoberts.mlw"/>
911
<theory name="ChangRoberts" proved="true">
1012
<goal name="next&#39;vc" expl="VC for next" proved="true">
11-
<proof prover="4" timelimit="5"><result status="valid" time="0.060000" steps="1012"/></proof>
13+
<proof prover="4"><result status="valid" time="0.060000" steps="1012"/></proof>
1214
</goal>
1315
<goal name="pred&#39;vc" expl="VC for pred" proved="true">
14-
<proof prover="4" timelimit="5"><result status="valid" time="0.030000" steps="1011"/></proof>
16+
<proof prover="4"><result status="valid" time="0.030000" steps="1011"/></proof>
1517
</goal>
1618
<goal name="initWorld&#39;vc" expl="VC for initWorld" proved="true">
17-
<proof prover="4" timelimit="5"><result status="valid" time="0.010000" steps="93"/></proof>
19+
<proof prover="4"><result status="valid" time="0.010000" steps="93"/></proof>
1820
</goal>
1921
<goal name="act&#39;vc" expl="VC for act" proved="true">
2022
<transf name="unfold" proved="true" arg1="inv">
2123
<goal name="act&#39;vc.0" expl="VC for act" proved="true">
2224
<transf name="split_all_full" proved="true" >
2325
<goal name="act&#39;vc.0.0" expl="unreachable point" proved="true">
24-
<proof prover="4"><result status="valid" time="0.010000" steps="58"/></proof>
26+
<proof prover="4" timelimit="1"><result status="valid" time="0.010000" steps="58"/></proof>
2527
</goal>
2628
<goal name="act&#39;vc.0.1" expl="precondition" proved="true">
27-
<proof prover="4"><result status="valid" time="0.010000" steps="23"/></proof>
29+
<proof prover="4" timelimit="1"><result status="valid" time="0.010000" steps="23"/></proof>
2830
</goal>
2931
<goal name="act&#39;vc.0.2" expl="precondition" proved="true">
30-
<proof prover="4"><result status="valid" time="0.010000" steps="23"/></proof>
32+
<proof prover="4" timelimit="1"><result status="valid" time="0.010000" steps="23"/></proof>
3133
</goal>
3234
<goal name="act&#39;vc.0.3" expl="postcondition" proved="true">
33-
<proof prover="3"><result status="valid" time="0.270000" steps="20891"/></proof>
35+
<transf name="split_vc" proved="true" >
36+
<goal name="act&#39;vc.0.3.0" expl="postcondition" proved="true">
37+
<transf name="split_vc" proved="true" >
38+
<goal name="act&#39;vc.0.3.0.0" expl="postcondition" proved="true">
39+
<proof prover="3" timelimit="20"><result status="valid" time="0.538522" steps="68104"/></proof>
40+
</goal>
41+
</transf>
42+
</goal>
43+
<goal name="act&#39;vc.0.3.1" expl="postcondition" proved="true">
44+
<transf name="split_vc" proved="true" >
45+
<goal name="act&#39;vc.0.3.1.0" expl="postcondition" proved="true">
46+
<proof prover="3" memlimit="2000"><result status="valid" time="0.301175" steps="42950"/></proof>
47+
</goal>
48+
</transf>
49+
</goal>
50+
</transf>
3451
</goal>
3552
<goal name="act&#39;vc.0.4" expl="postcondition" proved="true">
36-
<proof prover="4"><result status="valid" time="0.010000" steps="76"/></proof>
37-
</goal>
38-
<goal name="act&#39;vc.0.5" expl="postcondition" proved="true">
39-
<proof prover="4"><result status="valid" time="0.740736" steps="7080"/></proof>
40-
</goal>
41-
<goal name="act&#39;vc.0.6" expl="postcondition" proved="true">
4253
<transf name="split_vc" proved="true" >
43-
<goal name="act&#39;vc.0.6.0" expl="postcondition" proved="true">
44-
<proof prover="4"><result status="valid" time="0.090000" steps="1127"/></proof>
54+
<goal name="act&#39;vc.0.4.0" expl="postcondition" proved="true">
55+
<proof prover="0"><result status="valid" time="0.328621" steps="5026"/></proof>
4556
</goal>
4657
</transf>
4758
</goal>
48-
<goal name="act&#39;vc.0.7" expl="postcondition" proved="true">
49-
<proof prover="3"><result status="valid" time="0.280000" steps="21542"/></proof>
50-
</goal>
51-
<goal name="act&#39;vc.0.8" expl="postcondition" proved="true">
52-
<proof prover="4"><result status="valid" time="0.050000" steps="730"/></proof>
53-
</goal>
54-
<goal name="act&#39;vc.0.9" expl="postcondition" proved="true">
59+
<goal name="act&#39;vc.0.5" expl="postcondition" proved="true">
5560
<transf name="split_vc" proved="true" >
56-
<goal name="act&#39;vc.0.9.0" expl="postcondition" proved="true">
61+
<goal name="act&#39;vc.0.5.0" expl="postcondition" proved="true">
5762
<transf name="split_vc" proved="true" >
58-
<goal name="act&#39;vc.0.9.0.0" expl="postcondition" proved="true">
59-
<proof prover="3" timelimit="20"><result status="valid" time="1.970432" steps="125188"/></proof>
63+
<goal name="act&#39;vc.0.5.0.0" expl="postcondition" proved="true">
64+
<proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="23.889676" steps="1449758"/></proof>
6065
</goal>
6166
</transf>
6267
</goal>
63-
<goal name="act&#39;vc.0.9.1" expl="postcondition" proved="true">
68+
<goal name="act&#39;vc.0.5.1" expl="postcondition" proved="true">
6469
<transf name="split_vc" proved="true" >
65-
<goal name="act&#39;vc.0.9.1.0" expl="postcondition" proved="true">
66-
<proof prover="3" memlimit="2000"><result status="valid" time="4.316190" steps="275770"/></proof>
70+
<goal name="act&#39;vc.0.5.1.0" expl="postcondition" proved="true">
71+
<transf name="inline_goal" proved="true" >
72+
<goal name="act&#39;vc.0.5.1.0.0" expl="postcondition" proved="true">
73+
<transf name="split_all_full" proved="true" >
74+
<goal name="act&#39;vc.0.5.1.0.0.0" expl="postcondition" proved="true">
75+
<proof prover="3" timelimit="1"><result status="valid" time="0.605309" steps="98620"/></proof>
76+
</goal>
77+
</transf>
78+
</goal>
79+
</transf>
6780
</goal>
6881
</transf>
6982
</goal>
7083
</transf>
7184
</goal>
72-
<goal name="act&#39;vc.0.10" expl="postcondition" proved="true">
73-
<proof prover="4"><result status="valid" time="0.020000" steps="84"/></proof>
74-
</goal>
75-
<goal name="act&#39;vc.0.11" expl="postcondition" proved="true">
76-
<proof prover="3"><result status="valid" time="0.260000" steps="21004"/></proof>
77-
</goal>
78-
<goal name="act&#39;vc.0.12" expl="postcondition" proved="true">
79-
<proof prover="4"><result status="valid" time="0.020000" steps="80"/></proof>
85+
<goal name="act&#39;vc.0.6" expl="postcondition" proved="true">
86+
<transf name="split_vc" proved="true" >
87+
<goal name="act&#39;vc.0.6.0" expl="postcondition" proved="true">
88+
<proof prover="4" timelimit="1"><result status="valid" time="0.090000" steps="71"/></proof>
89+
</goal>
90+
</transf>
8091
</goal>
81-
<goal name="act&#39;vc.0.13" expl="postcondition" proved="true">
82-
<proof prover="4" timelimit="5"><result status="valid" time="0.590000" steps="7094"/></proof>
92+
<goal name="act&#39;vc.0.7" expl="postcondition" proved="true">
93+
<proof prover="1"><result status="valid" time="0.529864"/></proof>
8394
</goal>
84-
<goal name="act&#39;vc.0.14" expl="postcondition" proved="true">
85-
<proof prover="4"><result status="valid" time="0.010000" steps="42"/></proof>
95+
<goal name="act&#39;vc.0.8" expl="postcondition" proved="true">
96+
<proof prover="4" timelimit="1"><result status="valid" time="0.010000" steps="38"/></proof>
8697
</goal>
8798
</transf>
8899
</goal>
89100
</transf>
90101
</goal>
91102
<goal name="Refinement.initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
92-
<proof prover="4" timelimit="5"><result status="valid" time="0.010000" steps="74"/></proof>
103+
<proof prover="4"><result status="valid" time="0.010000" steps="74"/></proof>
93104
</goal>
94105
<goal name="Refinement.initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
95-
<proof prover="4" timelimit="5"><result status="valid" time="1.662458" steps="20280"/></proof>
106+
<proof prover="4"><result status="valid" time="2.099651" steps="39223"/></proof>
96107
</goal>
97108
<goal name="Refinement.stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
98-
<proof prover="4" timelimit="5"><result status="valid" time="0.010000" steps="85"/></proof>
109+
<proof prover="4"><result status="valid" time="0.010000" steps="85"/></proof>
99110
</goal>
100111
<goal name="Refinement.stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
101-
<proof prover="4" timelimit="5"><result status="valid" time="0.020000" steps="429"/></proof>
112+
<proof prover="4"><result status="valid" time="0.020000" steps="439"/></proof>
102113
</goal>
103114
<goal name="uniqueLeader" proved="true">
104-
<proof prover="4" timelimit="5"><result status="valid" time="0.020000" steps="212"/></proof>
115+
<proof prover="4"><result status="valid" time="0.020000" steps="211"/></proof>
105116
</goal>
106117
</theory>
107118
</file>

‎examples/leaderElection/ChangRoberts/why3shapes.gz‎

-609 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)