Set likely values for proof runtimes

Signed-off-by: Andrew Helwer <ahelwer@pm.me>

Author: ahelwer

.github/workflows/CI.yml

@@ -146,7 +146,8 @@ jobs:
             | map(select(has("proof")))
             # Failing on Linux
             | map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
-            | map(select(.proof.maxRuntimeMinutes <= 1))
+            # Skip long-running proofs in CI
+            | map(select(.proof.maxRuntimeMinutes <= 5))
             | map((.proof.maxRuntimeMinutes | tostring) + "\u0000" + .path + "\u0000")
             | join("")' \
           | xargs --verbose --null --no-run-if-empty -n 2 \

specifications/Bakery-Boulangerie/manifest.json

@@ -13,7 +13,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:20"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -23,7 +23,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:30"
+        "maxRuntimeMinutes": 1
       }
     },
     {

specifications/CigaretteSmokers/manifest.json

@@ -39,7 +39,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]

specifications/CoffeeCan/manifest.json

@@ -56,7 +56,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]

specifications/DieHard/manifest.json

@@ -36,6 +36,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/DieHard/DieHard_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/DieHard/DieHarder.tla",
       "features": [],
@@ -70,14 +78,6 @@
           "workers": 1
         }
       ]
-    },
-    {
-      "path": "specifications/DieHard/DieHard_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
 }

specifications/Disruptor/manifest.json

@@ -19,11 +19,6 @@
         }
       ]
     },
-    {
-      "path": "specifications/Disruptor/APRingBuffer.tla",
-      "features": [],
-      "models": []
-    },
     {
       "path": "specifications/Disruptor/APDisruptor_SPMC.tla",
       "features": [],
@@ -36,6 +31,11 @@
         }
       ]
     },
+    {
+      "path": "specifications/Disruptor/APRingBuffer.tla",
+      "features": [],
+      "models": []
+    },
     {
       "path": "specifications/Disruptor/Disruptor_MPMC.tla",
       "features": [],

specifications/FiniteMonotonic/manifest.json

@@ -50,7 +50,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {

specifications/KeyValueStore/manifest.json

@@ -28,6 +28,14 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/KeyValueStore/KeyValueStore_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/KeyValueStore/MCKVS.tla",
       "features": [],
@@ -68,14 +76,6 @@
       "path": "specifications/KeyValueStore/Util.tla",
       "features": [],
       "models": []
-    },
-    {
-      "path": "specifications/KeyValueStore/KeyValueStore_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
 }

specifications/LearnProofs/manifest.json

@@ -14,7 +14,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -24,7 +24,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:10"
+        "maxRuntimeMinutes": 1
       }
     },
     {

specifications/LoopInvariance/manifest.json

@@ -16,7 +16,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -56,7 +56,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:05:00"
+        "maxRuntimeMinutes": 10
       }
     },
     {
@@ -66,8 +66,8 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:01:30"
+        "maxRuntimeMinutes": 3
       }
     }
   ]
-}
+}