@@ -209,6 +209,13 @@ instance StateModel (Lockstep Model) where
209209 ADuplicate :: ModelVar Model (LSM RealWorld )
210210 -> Action (Lockstep Model ) (LSM RealWorld )
211211
212+ -- | Without this, the prototype only completes tiering merges when the next
213+ -- merging run on this level is created, so a level would never contain a
214+ -- completed merge.
215+ ASupply :: ModelVar Model (LSM RealWorld )
216+ -> Int
217+ -> Action (Lockstep Model ) ()
218+
212219 ADump :: ModelVar Model (LSM RealWorld )
213220 -> Action (Lockstep Model ) (Map Key Value )
214221
@@ -249,6 +256,7 @@ instance InLockstep Model where
249256 usedVars (ALookup v evk) = SomeGVar v
250257 : case evk of Left vk -> [SomeGVar vk]; _ -> []
251258 usedVars (ADuplicate v) = [SomeGVar v]
259+ usedVars (ASupply v _) = [SomeGVar v]
252260 usedVars (ADump v) = [SomeGVar v]
253261
254262 modelNextState = runModel
@@ -297,10 +305,13 @@ instance InLockstep Model where
297305 , not (null kvars)
298306 ]
299307 ++ [ (1 , fmap Some $
300- ADump <$> elements vars)
308+ ADuplicate <$> elements vars)
301309 ]
302310 ++ [ (1 , fmap Some $
303- ADuplicate <$> elements vars)
311+ ASupply <$> elements vars <*> (getSmall . getPositive <$> arbitrary))
312+ ]
313+ ++ [ (1 , fmap Some $
314+ ADump <$> elements vars)
304315 ]
305316
306317 shrinkWithVars _findVars _model (AInsert var (Right k) v) =
@@ -325,15 +336,17 @@ instance RunLockstep Model IO where
325336 (AInsert {}, x) -> OId x
326337 (ADelete {}, x) -> OId x
327338 (ALookup {}, x) -> OId x
328- (ADump {}, x) -> OId x
329339 (ADuplicate {}, _) -> ORef
340+ (ASupply {}, x) -> OId x
341+ (ADump {}, x) -> OId x
330342
331343 showRealResponse _ ANew = Nothing
332344 showRealResponse _ AInsert {} = Just Dict
333345 showRealResponse _ ADelete {} = Just Dict
334346 showRealResponse _ ALookup {} = Just Dict
335- showRealResponse _ ADump {} = Just Dict
336347 showRealResponse _ ADuplicate {} = Nothing
348+ showRealResponse _ ASupply {} = Nothing
349+ showRealResponse _ ADump {} = Just Dict
337350
338351deriving stock instance Show (Action (Lockstep Model ) a )
339352deriving stock instance Show (Observable Model a )
@@ -358,6 +371,7 @@ runActionIO action lookUp =
358371 ALookup var evk -> lookupResultValue <$> lookup (lookUpVar var) k
359372 where k = either lookUpVar id evk
360373 ADuplicate var -> duplicate (lookUpVar var)
374+ ASupply var n -> supply (lookUpVar var) n
361375 ADump var -> logicalValue (lookUpVar var)
362376 where
363377 lookUpVar :: ModelVar Model a -> a
@@ -393,6 +407,8 @@ runModel action lookUp m =
393407 ADuplicate var -> (MLSM mlsm', m')
394408 where (mlsm', m') = modelDuplicate (lookUpLsMVar var) m
395409
410+ ASupply _ _ -> (MUnit () , m) -- noop
411+
396412 ADump var -> (MDump mapping, m)
397413 where (mapping, _) = modelDump (lookUpLsMVar var) m
398414 where
0 commit comments