@@ -89,7 +89,6 @@ prop_traces =
89
89
& cover 1 (countContests steps >= 2 ) " has multiple contests"
90
90
& cover 5 (closeNonInitial steps) " close with non initial snapshots"
91
91
& cover 5 (hasDecrement steps) " has successful decrements"
92
- & cover 1 (hasNegativeDecrement steps) " has negative decrements"
93
92
where
94
93
hasFanout =
95
94
any $
@@ -125,13 +124,7 @@ prop_traces =
125
124
hasDecrement =
126
125
any $
127
126
\ (_ := ActionWithPolarity {polarAction, polarity}) -> case polarAction of
128
- Decrement {} -> polarity == PosPolarity
129
- _ -> False
130
-
131
- hasNegativeDecrement =
132
- any $
133
- \ (_ := ActionWithPolarity {polarAction, polarity}) -> case polarAction of
134
- Decrement {} -> polarity == NegPolarity
127
+ Decrement {snapshot} -> polarity == PosPolarity && (not . null $ decommitUTxO snapshot)
135
128
_ -> False
136
129
137
130
prop_runActions :: Actions Model -> Property
@@ -227,33 +220,38 @@ instance StateModel Model where
227
220
arbitraryAction _lookup Model {headState, latestSnapshot, utxoInHead} =
228
221
case headState of
229
222
Open {} ->
230
- oneof $
231
- [ do
232
- actor <- elements allActors
233
- someUTxOToDecrement <-
234
- if not (null utxoInHead) then oneof $ pure <$> [utxoInHead] else pure $ Set. fromList []
235
-
236
- snapshot <-
237
- ModelSnapshot
238
- { snapshotNumber = latestSnapshot
239
- , snapshotUTxO = utxoInHead
240
- , decommitUTxO = someUTxOToDecrement
241
- }
242
- `orArbitrary` arbitrary
243
- pure $ Some $ Close {actor, snapshot}
244
- ]
245
- <> [ do
223
+ frequency $
224
+ [
225
+ ( 1
226
+ , do
246
227
actor <- elements allActors
247
- someUTxOToDecrement <- oneof $ pure <$> Set. toList utxoInHead
228
+ someUTxOToDecrement <-
229
+ if not (null utxoInHead) then oneof $ pure <$> [utxoInHead] else pure $ Set. fromList []
248
230
snapshot <-
249
231
ModelSnapshot
250
- { snapshotNumber = latestSnapshot + 1
251
- , snapshotUTxO = Set. delete someUTxOToDecrement utxoInHead
252
- , decommitUTxO = Set. fromList [ someUTxOToDecrement]
232
+ { snapshotNumber = latestSnapshot
233
+ , snapshotUTxO = utxoInHead
234
+ , decommitUTxO = someUTxOToDecrement
253
235
}
254
236
`orArbitrary` arbitrary
255
- pure $ Some Decrement {actor, snapshot}
256
- | not (null utxoInHead)
237
+ pure $ Some $ Close {actor, snapshot}
238
+ )
239
+ ]
240
+ <> [
241
+ ( 10
242
+ , do
243
+ actor <- elements allActors
244
+ someUTxOToDecrement <-
245
+ if not (null utxoInHead) then oneof $ pure <$> [utxoInHead] else pure $ Set. fromList []
246
+ snapshot <-
247
+ ModelSnapshot
248
+ { snapshotNumber = latestSnapshot + 1
249
+ , snapshotUTxO = utxoInHead Set. \\ someUTxOToDecrement
250
+ , decommitUTxO = someUTxOToDecrement
251
+ }
252
+ `orMoreOftenArbitrary` arbitrary
253
+ pure $ Some Decrement {actor, snapshot}
254
+ )
257
255
]
258
256
Closed {} ->
259
257
oneof $
@@ -313,23 +311,10 @@ instance StateModel Model where
313
311
-- False, the action is discarded (e.g. it's invalid or we don't want to see
314
312
-- it tried to perform).
315
313
validFailingAction :: Model -> Action Model a -> Bool
316
- validFailingAction Model {headState, latestSnapshot, alreadyContested, utxoInHead} = \ case
314
+ validFailingAction Model {headState, utxoInHead} = \ case
317
315
Decrement {snapshot} ->
318
316
headState == Open
319
317
&& decommitUTxO snapshot `Set.isSubsetOf` utxoInHead
320
- -- Close{snapshot} ->
321
- -- headState == Open
322
- -- && snapshotNumber snapshot < latestSnapshot
323
- -- Contest{actor, snapshot} ->
324
- -- headState == Closed
325
- -- && ( snapshotNumber snapshot <= latestSnapshot
326
- -- | | actor `elem` alreadyContested
327
- -- )
328
- -- Fanout{snapshot} ->
329
- -- headState == Closed
330
- -- && ( snapshotNumber snapshot /= latestSnapshot
331
- -- | | snapshotUTxO snapshot /= utxoInHead
332
- -- )
333
318
_ -> True
334
319
335
320
nextState :: Model -> Action Model a -> Var a -> Model
@@ -720,3 +705,6 @@ expectInvalid = \case
720
705
-- the given value.
721
706
orArbitrary :: a -> Gen a -> Gen a
722
707
orArbitrary a gen = frequency [(1 , pure a), (1 , gen)]
708
+
709
+ orMoreOftenArbitrary :: a -> Gen a -> Gen a
710
+ orMoreOftenArbitrary a gen = frequency [(1 , pure a), (10 , gen)]
0 commit comments