Skip to content

Commit efc7c40

Browse files
jorisdralmheinzel
jorisdral
authored and
mheinzel
committed
QLS: fix SupplyPortionOfDebt 
1 parent 7833014 commit efc7c40

File tree

1 file changed

+45
-28
lines changed

1 file changed

+45
-28
lines changed

‎test/Test/Database/LSMTree/StateMachine.hs‎

Lines changed: 45 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -761,8 +761,8 @@ data Action' h a where
761761
-- 'SupplyUnionCredits' gets no information about union debt, so the union
762762
-- credits we generate are arbitrary, and it would require precarious, manual
763763
-- tuning to make sure the debt is ever paid off by an action sequence.
764-
-- 'SupplyUnionCredits' supplies a portion (if not al) of the current debt, so
765-
-- that unions are more likely to finish during a sequence of actions.
764+
-- 'SupplyUnionCredits' supplies a portion (if not all) of the current debt,
765+
-- so that unions are more likely to finish during a sequence of actions.
766766
SupplyPortionOfDebt ::
767767
C k v b
768768
=> Var h (WrapTable h IO k v b)
@@ -904,6 +904,7 @@ instance ( Eq (Class.TableConfig h)
904904
MSnapshotName :: R.SnapshotName -> Val h R.SnapshotName
905905
MUnionDebt :: R.UnionDebt -> Val h R.UnionDebt
906906
MUnionCredits :: R.UnionCredits -> Val h R.UnionCredits
907+
MUnionCreditsPortion :: R.UnionCredits -> Val h R.UnionCredits
907908
MErr :: Model.Err -> Val h Model.Err
908909
-- combinators
909910
MUnit :: () -> Val h ()
@@ -926,6 +927,8 @@ instance ( Eq (Class.TableConfig h)
926927
-> Obs h (QueryResult k v (WrapBlobRef h IO b))
927928
OBlob :: (Show b, Typeable b, Eq b)
928929
=> WrapBlob b -> Obs h (WrapBlob b)
930+
OUnionCredits :: R.UnionCredits -> Obs h R.UnionCredits
931+
OUnionCreditsPortion :: R.UnionCredits -> Obs h R.UnionCredits
929932
OId :: (Show a, Typeable a, Eq a) => a -> Obs h a
930933
-- combinators
931934
OPair :: (Obs h a, Obs h b) -> Obs h (a, b)
@@ -935,21 +938,22 @@ instance ( Eq (Class.TableConfig h)
935938

936939
observeModel :: Val h a -> Obs h a
937940
observeModel = \case
938-
MTable _ -> OTable
939-
MCursor _ -> OCursor
940-
MBlobRef _ -> OBlobRef
941-
MLookupResult x -> OLookupResult $ fmap observeModel x
942-
MQueryResult x -> OQueryResult $ fmap observeModel x
943-
MSnapshotName x -> OId x
944-
MBlob x -> OBlob x
945-
MUnionDebt x -> OId x
946-
MUnionCredits x -> OId x
947-
MErr x -> OId x
948-
MUnit x -> OId x
949-
MPair x -> OPair $ bimap observeModel observeModel x
950-
MEither x -> OEither $ bimap observeModel observeModel x
951-
MList x -> OList $ map observeModel x
952-
MVector x -> OVector $ V.map observeModel x
941+
MTable _ -> OTable
942+
MCursor _ -> OCursor
943+
MBlobRef _ -> OBlobRef
944+
MLookupResult x -> OLookupResult $ fmap observeModel x
945+
MQueryResult x -> OQueryResult $ fmap observeModel x
946+
MSnapshotName x -> OId x
947+
MBlob x -> OBlob x
948+
MUnionDebt x -> OId x
949+
MUnionCredits x -> OUnionCredits x
950+
MUnionCreditsPortion x -> OUnionCreditsPortion x
951+
MErr x -> OId x
952+
MUnit x -> OId x
953+
MPair x -> OPair $ bimap observeModel observeModel x
954+
MEither x -> OEither $ bimap observeModel observeModel x
955+
MList x -> OList $ map observeModel x
956+
MVector x -> OVector $ V.map observeModel x
953957

954958
modelNextState :: forall a.
955959
LockstepAction (ModelState h) a
@@ -1047,27 +1051,38 @@ instance Eq (Obs h a) where
10471051
, Just Model.DefaultErrSnapshotCorrupted <- cast rhs
10481052
-> True
10491053

1054+
-- RemainingUnionDebt
1055+
--
10501056
-- Debt in the model is always 0, while debt in the real implementation
10511057
-- may be larger than 0.
10521058
(OEither (Right (OId lhs)), OEither (Right (OId rhs)))
10531059
| Just (lhsDebt :: R.UnionDebt) <- cast lhs
10541060
, Just (rhsDebt :: R.UnionDebt) <- cast rhs
1055-
-> lhsDebt >= rhsDebt
1061+
-> lhsDebt >= R.UnionDebt 0 && rhsDebt == R.UnionDebt 0
10561062

1063+
-- SupplyUnionCredits
1064+
--
10571065
-- In the model, all supplied union credits are returned as leftovers,
1058-
-- whereas in the real implementation may use up some union credits.
1059-
(OEither (Right (OId lhs)), OEither (Right (OId rhs)))
1060-
| Just (lhsLeftovers :: R.UnionCredits) <- cast lhs
1061-
, Just (rhsLeftovers :: R.UnionCredits) <- cast rhs
1066+
-- whereas the real implementation may use up some union credits.
1067+
(OEither (Right (OUnionCredits lhsLeftovers)), OEither (Right (OUnionCredits rhsLeftovers)))
10621068
-> lhsLeftovers <= rhsLeftovers
10631069

1070+
-- SupplyPortionOfDebt
1071+
--
1072+
-- In the model, a portion of the debt is always 0, whereas in the real
1073+
-- implementation the portion of the debt is non-negative.
1074+
(OEither (Right (OUnionCreditsPortion lhsLeftovers)), OEither (Right (OUnionCreditsPortion rhsLeftovers)))
1075+
-> lhsLeftovers >= rhsLeftovers
1076+
10641077
-- default equalities
10651078
(OTable, OTable) -> True
10661079
(OCursor, OCursor) -> True
10671080
(OBlobRef, OBlobRef) -> True
10681081
(OLookupResult x, OLookupResult y) -> x == y
10691082
(OQueryResult x, OQueryResult y) -> x == y
10701083
(OBlob x, OBlob y) -> x == y
1084+
(OUnionCredits x, OUnionCredits y) -> x == y
1085+
(OUnionCreditsPortion x, OUnionCreditsPortion y) -> x == y
10711086
(OId x, OId y) -> x == y
10721087
(OPair x, OPair y) -> x == y
10731088
(OEither x, OEither y) -> x == y
@@ -1083,6 +1098,8 @@ instance Eq (Obs h a) where
10831098
OLookupResult{} -> ()
10841099
OQueryResult{} -> ()
10851100
OBlob{} -> ()
1101+
OUnionCredits{} -> ()
1102+
OUnionCreditsPortion{} -> ()
10861103
OId{} -> ()
10871104
OPair{} -> ()
10881105
OEither{} -> ()
@@ -1175,8 +1192,8 @@ instance ( Eq (Class.TableConfig h)
11751192
Union{} -> OEither $ bimap OId (const OTable) result
11761193
Unions{} -> OEither $ bimap OId (const OTable) result
11771194
RemainingUnionDebt{} -> OEither $ bimap OId OId result
1178-
SupplyUnionCredits{} -> OEither $ bimap OId OId result
1179-
SupplyPortionOfDebt{} -> OEither $ bimap OId OId result
1195+
SupplyUnionCredits{} -> OEither $ bimap OId OUnionCredits result
1196+
SupplyPortionOfDebt{} -> OEither $ bimap OId OUnionCreditsPortion result
11801197

11811198
showRealResponse ::
11821199
Proxy (RealMonad h IO)
@@ -1241,8 +1258,8 @@ instance ( Eq (Class.TableConfig h)
12411258
Union{} -> OEither $ bimap OId (const OTable) result
12421259
Unions{} -> OEither $ bimap OId (const OTable) result
12431260
RemainingUnionDebt{} -> OEither $ bimap OId OId result
1244-
SupplyUnionCredits{} -> OEither $ bimap OId OId result
1245-
SupplyPortionOfDebt{} -> OEither $ bimap OId OId result
1261+
SupplyUnionCredits{} -> OEither $ bimap OId OUnionCredits result
1262+
SupplyPortionOfDebt{} -> OEither $ bimap OId OUnionCreditsPortion result
12461263

12471264
showRealResponse ::
12481265
Proxy (RealMonad h (IOSim s))
@@ -1418,7 +1435,7 @@ runModel lookUp (Action merrs action') = case action' of
14181435
(Model.supplyUnionCredits (getTable $ lookUp tableVar) credits)
14191436
(pure ()) -- TODO(err)
14201437
SupplyPortionOfDebt tableVar portion ->
1421-
wrap MUnionCredits
1438+
wrap MUnionCreditsPortion
14221439
. Model.runModelMWithInjectedErrors merrs
14231440
(do let table = getTable $ lookUp tableVar
14241441
debt <- Model.remainingUnionDebt table
@@ -2181,7 +2198,7 @@ shrinkAction'WithVars _ctx _st a = case a of
21812198
-- the union debt is larger.
21822199
SupplyPortionOfDebt tableVar (Portion x) -> [
21832200
Some $ SupplyUnionCredits tableVar (R.UnionCredits x')
2184-
| x' <- [2 ^ i - 1 | (i :: Int) <- [0..63]]
2201+
| x' <- [2 ^ i - 1 | (i :: Int) <- [0..20]]
21852202
, assert (x' >= 0) True
21862203
] ++ [
21872204
Some $ SupplyPortionOfDebt tableVar (Portion x')

0 commit comments

Comments
 (0)