update proofs

haslab · Mar 8, 2024 · 44773aa · 44773aa
1 parent 36f929f
commit 44773aa
Show file tree

Hide file tree

Showing 6 changed files with 20 additions and 8 deletions.
diff --git a/examples/distributedLockNetwork/LDTDupl/why3session.xml b/examples/distributedLockNetwork/LDTDupl/why3session.xml
@@ -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>

diff --git a/examples/leaderElection/ChangRoberts/why3session.xml b/examples/leaderElection/ChangRoberts/why3session.xml
@@ -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>

diff --git a/examples/paxosNoRefinement/paxos/why3session.xml b/examples/paxosNoRefinement/paxos/why3session.xml
@@ -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">

diff --git a/examples/paxosNoRefinement/paxos/why3shapes.gz b/examples/paxosNoRefinement/paxos/why3shapes.gz
diff --git a/examples/waitFreeRegister/fourSlots/why3session.xml b/examples/waitFreeRegister/fourSlots/why3session.xml
@@ -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>

diff --git a/test.sh b/test.sh
@@ -13,14 +13,14 @@ all_tests=(
 "examples/mutualExclusionConcurrent/PetersonAtomic -L stateMachineModels -L examples/mutualExclusionConcurrent"
 "examples/mutualExclusionConcurrent/BakeryAtomic -L stateMachineModels -L examples/mutualExclusionConcurrent"
 "examples/waitFreeRegister/slotsAbstract -L stateMachineModels -L examples/waitFreeRegister"
-# "examples/waitFreeRegister/fourSlots -L stateMachineModels -L examples/waitFreeRegister"
+"examples/waitFreeRegister/fourSlots -L stateMachineModels -L examples/waitFreeRegister"
 "examples/counter/counter -L stateMachineModels -L examples/counter"
 "examples/counter/counter_lock -L stateMachineModels -L examples/counter"
 "examples/counter/counter_alt -L stateMachineModels -L examples/counter"
 "examples/counter/counter_lock_alt -L stateMachineModels -L examples/counter"
 "examples/leaderElection/leaderElect -L stateMachineModels -L examples/leaderElection"
 "examples/leaderElection/leaderElectMax -L stateMachineModels -L examples/leaderElection"
-# "examples/leaderElection/ChangRoberts -L stateMachineModels -L examples/leaderElection"
+"examples/leaderElection/ChangRoberts -L stateMachineModels -L examples/leaderElection"
 "examples/leaderElection/ChangRobertsNetwork -L stateMachineModels -L examples/leaderElection"
 "examples/mutualExclusionToken/oneToken -L stateMachineModels -L examples/mutualExclusionToken"
 # "examples/mutualExclusionToken/selfstab-ring -L stateMachineModels -L examples/mutualExclusionToken"
@@ -35,8 +35,8 @@ all_tests=(
 "examples/changRobertsNetwork/leaderlect-ring -L networkModels"
 "examples/distributedLockNetwork/specLDT"
 "examples/distributedLockNetwork/LDT -L networkModels -L examples/distributedLockNetwork"
-# "examples/distributedLockNetwork/LDTDupl -L networkModels -L examples/distributedLockNetwork"
-# "examples/paxosNoRefinement/paxos"
+"examples/distributedLockNetwork/LDTDupl -L networkModels -L examples/distributedLockNetwork"
+"examples/paxosNoRefinement/paxos"
 )
 
 failed=0