@@ -673,12 +673,13 @@ instance ( Eq (Class.TableConfig h)
673673 -> ModelLookUp (ModelState h )
674674 -> ModelState h
675675 -> (ModelValue (ModelState h ) a , ModelState h )
676- modelNextState action lookUp (ModelState mock stats) =
677- auxStats $ runModel lookUp action mock
676+ modelNextState action lookUp (ModelState state stats) =
677+ auxStats $ runModel lookUp action state
678678 where
679679 auxStats :: (Val h a , Model. Model ) -> (Val h a , ModelState h )
680- auxStats (result, state') =
681- (result, ModelState state' $ updateStats action lookUp result stats)
680+ auxStats (result, state') = (result, ModelState state' stats')
681+ where
682+ stats' = updateStats action lookUp state state' result stats
682683
683684 usedVars :: LockstepAction (ModelState h ) a -> [AnyGVar (ModelOp (ModelState h ))]
684685 usedVars = \ case
@@ -1315,6 +1316,10 @@ data Stats = Stats {
13151316 -- === Final tags (per action sequence, per table)
13161317 -- | Number of actions per table (succesful or failing)
13171318 , numActionsPerTable :: ! (Map Model. TableHandleID Int )
1319+ -- | The size of tables that were closed. This is used to augment the table
1320+ -- sizes from the final model state (which of course has only tables still
1321+ -- open in the final state).
1322+ , closedTableSizes :: ! (Map Model. TableHandleID Int )
13181323 }
13191324 deriving stock Show
13201325
@@ -1329,6 +1334,7 @@ initStats = Stats {
13291334 , successActions = []
13301335 , failActions = []
13311336 , numActionsPerTable = Map. empty
1337+ , closedTableSizes = Map. empty
13321338 }
13331339
13341340updateStats ::
@@ -1340,10 +1346,12 @@ updateStats ::
13401346 )
13411347 => LockstepAction (ModelState h ) a
13421348 -> ModelLookUp (ModelState h )
1349+ -> Model. Model
1350+ -> Model. Model
13431351 -> Val h a
13441352 -> Stats
13451353 -> Stats
1346- updateStats action lookUp result =
1354+ updateStats action lookUp modelBefore _modelAfter result =
13471355 -- === Tags
13481356 updNewTableTypes
13491357 . updSnapshotted
@@ -1353,6 +1361,7 @@ updateStats action lookUp result =
13531361 . updSuccessActions
13541362 . updFailActions
13551363 . updNumActionsPerTable
1364+ . updClosedTableSizes
13561365 where
13571366 -- === Tags
13581367
@@ -1477,6 +1486,18 @@ updateStats action lookUp result =
14771486 (numActionsPerTable stats)
14781487 }
14791488
1489+ updClosedTableSizes stats = case action of
1490+ Close tableVar
1491+ | MTableHandle th <- lookUp tableVar
1492+ , let tid = Model. tableHandleID th
1493+ -- This lookup can fail if the table was already closed:
1494+ , Just (_, table) <- Map. lookup tid (Model. tableHandles modelBefore)
1495+ , let tsize = Model. withSomeTable Model. size table
1496+ -> stats {
1497+ closedTableSizes = Map. insert tid tsize (closedTableSizes stats)
1498+ }
1499+ _ -> stats
1500+
14801501 getTableHandleId :: ModelValue (ModelState h ) (WrapTableHandle h IO k v blob )
14811502 -> Model. TableHandleID
14821503 getTableHandleId (MTableHandle th) = Model. tableHandleID th
@@ -1594,18 +1615,19 @@ data FinalTag =
15941615 -- | Number of actions on each table
15951616 | NumTableActions String
15961617 -- | Total /logical/ size of a table
1597- | TableSize String -- TODO: implement
1618+ | TableSize String
15981619 deriving stock Show
15991620
16001621-- | This is run only after completing every action
16011622tagFinalState' :: Lockstep (ModelState h ) -> [(String , [FinalTag ])]
1602- tagFinalState' (getModel -> ModelState _ finalStats) = concat [
1623+ tagFinalState' (getModel -> ModelState finalState finalStats) = concat [
16031624 tagNumLookupsResults
16041625 , tagNumUpdates
16051626 , tagSuccessActions
16061627 , tagFailActions
16071628 , tagNumTables
16081629 , tagNumTableActions
1630+ , tagTableSizes
16091631 ]
16101632 where
16111633 tagNumLookupsResults = [
@@ -1640,6 +1662,15 @@ tagFinalState' (getModel -> ModelState _ finalStats) = concat [
16401662 | n <- Map. elems (numActionsPerTable finalStats)
16411663 ]
16421664
1665+ tagTableSizes =
1666+ [ (" Table sizes" , [ TableSize (showPowersOf 2 size) ])
1667+ | let openSizes, closedSizes :: Map Model. TableHandleID Int
1668+ openSizes = Model. withSomeTable Model. size . snd <$>
1669+ Model. tableHandles finalState
1670+ closedSizes = closedTableSizes finalStats
1671+ , size <- Map. elems (openSizes `Map.union` closedSizes)
1672+ ]
1673+
16431674{- ------------------------------------------------------------------------------
16441675 Utils
16451676-------------------------------------------------------------------------------}
0 commit comments