label MergingTree prop_supplyCredits

Author: mheinzel

src/Database/LSMTree/Internal/MergingRun.hs

@@ -761,8 +761,8 @@ atomicSpendCredits (CreditsVar var) spend =
 
 {-# SPECIALISE remainingMergeDebt ::
      Ref (MergingRun t IO h) -> IO (MergeDebt, NumEntries) #-}
--- | Calculate an upper bound on the merge credits required to complete the
--- merge, as well as an upper bound on the size of the resulting run.
+-- | Calculate the merge credits required to complete the merge, as well as an
+-- upper bound on the size of the resulting run.
 remainingMergeDebt ::
      (MonadMVar m, PrimMonad m)
   => Ref (MergingRun t m h) -> m (MergeDebt, NumEntries)

test/Test/Database/LSMTree/Internal/MergingTree.hs

@@ -14,6 +14,7 @@ import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Traversable (for)
 import qualified Data.Vector as V
+import           Database.LSMTree.Extras (showPowersOf10)
 import           Database.LSMTree.Extras.MergingRunData
 import           Database.LSMTree.Extras.MergingTreeData
 import           Database.LSMTree.Extras.RunData
@@ -229,22 +230,38 @@ prop_supplyCredits hfs hbio threshold credits mtd = do
     FS.createDirectory hfs (FS.mkFsPath ["active"])
     counter <- newUniqCounter 0
     withMergingTree hfs hbio resolveVal runParams setupPath counter mtd $ \tree -> do
+      (MR.MergeDebt initialDebt, _) <- remainingMergeDebt tree
       props <- for credits $ \c -> do
         (MR.MergeDebt debt, _) <- remainingMergeDebt tree
-        leftovers <-
-          supplyCredits hfs hbio resolveVal runParams threshold root counter tree c
-        (MR.MergeDebt debt', _) <- remainingMergeDebt tree
-        return $
-          counterexample (show (debt, leftovers, debt')) $ conjoin [
-              counterexample "negative values" $
-                debt >= 0 && leftovers >= 0 && debt' >= 0
-            , counterexample "did not reduce debt sufficiently" $
-                debt' <= debt - (c - leftovers)
-            ]
-      return (conjoin (toList props))
+        if debt <= 0
+          then
+            return $ property True
+          else do
+            leftovers <-
+              supplyCredits hfs hbio resolveVal runParams threshold root counter tree c
+            (MR.MergeDebt debt', _) <- remainingMergeDebt tree
+            return $
+              -- semi-useful, but mainly tells us in how many steps we supplied
+              tabulate "supplied credits" [showPowersOf10 (fromIntegral c)] $
+              counterexample (show (debt, leftovers, debt')) $ conjoin [
+                  counterexample "negative values" $
+                    debt >= 0 && leftovers >= 0 && debt' >= 0
+                , counterexample "did not reduce debt sufficiently" $
+                    debt' <= debt - (c - leftovers)
+                ]
+      (MR.MergeDebt finalDebt, _) <- remainingMergeDebt tree
+      return $
+        labelDebt initialDebt finalDebt $
+          conjoin (toList props)
   where
     root = Paths.SessionRoot (FS.mkFsPath [])
-    setupPath = FS.mkFsPath ["setup"]  -- separate dir, so it doesn't clash
+    setupPath = FS.mkFsPath ["setup"]  -- separate dir, so file paths in errors
+                                       -- are identifiable as created in setup
+                                       --
+    labelDebt initial final
+      | initial == 0 = label "trivial"
+      | final   == 0 = label "completed"
+      | otherwise    = label "incomplete"
 
 instance Arbitrary MR.MergeCredits where
   arbitrary = MR.MergeCredits . getPositive <$> arbitrary