diff --git a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs index 74f2ea2328f..08013bd822c 100644 --- a/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs +++ b/hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs @@ -1,13 +1,11 @@ -- | Stateful model-based testing of the transactions created by the "Direct" -- chain modules. -- --- FIXME: update description of tactics -- The model is focusing on transitions between Open and Closed states of the --- head right now. Snapshots are only modeled "in proxy" where we generate --- snapshot numbers and the fact whether they have something to decommit or not, --- but not the actual snapshot contents. All snapshots are correctly signed by a --- fixed list of participants and other fixtures are used for head parameters --- etc. +-- head right now. We have a simple UTxO model that consists of `SingleUTxO` +-- constructor and value is represented as a natural number. Snapshot versions +-- are tracked in the `AppM` monad (together with the _real_ Cardano UTxO) and +-- we update those on each successfull decommit transaction. module Hydra.Chain.Direct.TxTraceSpec where import Hydra.Prelude hiding (Any, State, label, show) @@ -89,10 +87,9 @@ prop_traces = True & cover 1 (null steps) "empty" & cover 10 (hasFanout steps) "reach fanout" - & cover 1 (fanoutWithEmptyUTxO steps) "fanout with empty UTxO" + & cover 0.1 (fanoutWithEmptyUTxO steps) "fanout with empty UTxO" & cover 5 (fanoutWithSomeUTxO steps) "fanout with some UTxO" - & cover 0.5 (fanoutWithDecrement steps) "fanout with something to decrement" - & cover 0.5 (fanoutWithSomeUTxOAndDecrement steps) "fanout with some UTxO and something to decrement" + & cover 5 (fanoutWithSomeUTxOToDecommit steps) "fanout with some UTxO to decommit" & cover 1 (countContests steps >= 2) "has multiple contests" & cover 5 (closeNonInitial steps) "close with non initial snapshots" & cover 5 (closeWithSomeUTxO steps) "close with some UTxO" @@ -103,6 +100,8 @@ prop_traces = where hasSnapshotUTxO snapshot = not . null $ snapshotUTxO snapshot + hasSnapshotUTxOToDecommit snapshot = not . null $ decommitUTxO snapshot + hasNoSnapshotUTxO snapshot = null $ snapshotUTxO snapshot hasDecommitValue snapshot = sum (Map.elems (decommitUTxO snapshot)) > 0 @@ -133,21 +132,11 @@ prop_traces = && hasSnapshotUTxO snapshot _ -> False - fanoutWithDecrement = - any $ - \(_ := ActionWithPolarity{polarAction, polarity}) -> case polarAction of - Fanout{snapshot} -> - polarity == PosPolarity - && hasDecommitValue snapshot - _ -> False - - fanoutWithSomeUTxOAndDecrement = + fanoutWithSomeUTxOToDecommit = any $ - \(_ := ActionWithPolarity{polarAction, polarity}) -> case polarAction of + \(_ := ActionWithPolarity{polarAction}) -> case polarAction of Fanout{snapshot} -> - polarity == PosPolarity - && hasSnapshotUTxO snapshot - && hasDecommitValue snapshot + hasSnapshotUTxOToDecommit snapshot _ -> False countContests = @@ -216,7 +205,7 @@ prop_runActions actions = -- * ============================== MODEL WORLD ========================== data SingleUTxO = A | B | C | D | E - deriving (Show, Eq, Ord, Enum, Generic) + deriving (Show, Eq, Ord, Enum, Bounded, Generic) instance Arbitrary SingleUTxO where arbitrary = genericArbitrary @@ -278,6 +267,11 @@ data TxResult = TxResult initialAmount :: Natural initialAmount = 10 +startingUTxO :: ModelUTxO +startingUTxO = + let utxo = [minBound .. maxBound] + in map (,initialAmount) utxo & Map.fromList + balanceUTxOInHead :: Ord k => Map k Natural -> Map k Natural -> Map k Natural balanceUTxOInHead currentUtxoInHead someUTxOToDecrement = currentUtxoInHead `Map.difference` someUTxOToDecrement @@ -297,7 +291,7 @@ instance StateModel Model where { headState = Open , latestSnapshot = 0 , alreadyContested = [] - , utxoInHead = fromList [(A, initialAmount)] + , utxoInHead = startingUTxO , decommitUTxOInHead = Map.empty } @@ -324,15 +318,21 @@ instance StateModel Model where not (null utxoInHead) ] Closed{} -> - oneof $ - [ do - snapshot <- genSnapshot - pure $ Some $ Fanout{snapshot} + frequency $ + [ + ( 5 + , do + snapshot <- genSnapshot + pure $ Some $ Fanout{snapshot} + ) ] - <> [ do - actor <- elements allActors - snapshot <- genSnapshot - pure $ Some Contest{actor, snapshot} + <> [ + ( 5 + , do + actor <- elements allActors + snapshot <- genSnapshot + pure $ Some Contest{actor, snapshot} + ) ] Final -> pure $ Some Stop where @@ -347,7 +347,8 @@ instance StateModel Model where , decommitUTxO = filteredSomeUTxOToDecrement } oneof - [ -- valid + [ arbitrary + , -- valid pure validSnapshot , -- unbalanced pure validSnapshot{snapshotUTxO = utxoInHead} @@ -374,7 +375,6 @@ instance StateModel Model where { snapshotUTxO = balancedUTxOInHead' , decommitUTxO = someUTxOToDecrement' } - , arbitrary ] genSubModelOf :: ModelUTxO -> Gen ModelUTxO @@ -431,7 +431,7 @@ instance StateModel Model where Contest{actor, snapshot} -> headState == Closed && actor `notElem` alreadyContested - && snapshotNumber snapshot > latestSnapshot + -- && snapshotNumber snapshot > latestSnapshot -- XXX: you are decrementing from existing utxo in the head && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot)) -- XXX: your tx is balanced with the utxo in the head @@ -868,8 +868,3 @@ expectInvalid = \case counterexample' $ renderTxWithUTxO spendableUTxO tx fail "But it did not fail" _ -> pure () - --- | Generate sometimes a value with given generator, bur more often just use --- the given value. -orArbitrary :: a -> Gen a -> Gen a -orArbitrary a gen = frequency [(1, pure a), (2, gen)]