Skip to content
This repository has been archived by the owner on Dec 2, 2024. It is now read-only.

Reactive state updates in contract models #67

Merged
merged 4 commits into from
Nov 2, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 15 additions & 4 deletions plutus-contract/src/Plutus/Contract/Test/ContractModel.hs
Original file line number Diff line number Diff line change
Expand Up @@ -320,6 +320,11 @@ class ( Typeable state
precondition :: ModelState state -> Action state -> Bool
precondition _ _ = True

-- | `nextReactiveState` is run every time the model `wait`s for a slot to be reached. This
-- can be used to model reactive components of off-chain code.
nextReactiveState :: Slot -> Spec state ()
nextReactiveState _ = return ()

-- | This is where the model logic is defined. Given an action, `nextState` specifies the
-- effects running that action has on the model state. It runs in the `Spec` monad, which is a
-- state monad over the `ModelState`.
Expand Down Expand Up @@ -456,12 +461,18 @@ modState :: forall state a. Setter' (ModelState state) a -> (a -> a) -> Spec sta
modState l f = Spec $ State.modify $ over l f

-- | Wait the given number of slots. Updates the `currentSlot` of the model state.
wait :: Integer -> Spec state ()
wait n = modState currentSlotL (+ Slot n)
wait :: ContractModel state => Integer -> Spec state ()
wait n = do
Slot now <- viewModelState currentSlot
nextReactiveState (Slot $ now + n)
modState currentSlotL (const (Slot $ now + n))

-- | Wait until the given slot. Has no effect if `currentSlot` is greater than the given slot.
waitUntil :: Slot -> Spec state ()
waitUntil n = modState currentSlotL (max n)
waitUntil :: ContractModel state => Slot -> Spec state ()
waitUntil (Slot n) = do
Slot now <- viewModelState currentSlot
when (now < n) $ do
wait (n - now)

-- | Mint tokens. Minted tokens start out as `lockedValue` (i.e. owned by the contract) and can be
-- transferred to wallets using `deposit`.
Expand Down
26 changes: 14 additions & 12 deletions plutus-use-cases/test/Spec/Auction.hs
Original file line number Diff line number Diff line change
Expand Up @@ -165,8 +165,8 @@ data AuctionModel = AuctionModel
{ _currentBid :: Integer
, _winner :: Wallet
, _endSlot :: Slot
, _phase :: Phase }
deriving (Show)
, _phase :: Phase
} deriving (Show)

data Phase = NotStarted | Bidding | AuctionOver
deriving (Eq, Show)
Expand Down Expand Up @@ -208,6 +208,16 @@ instance ContractModel AuctionModel where
WaitUntil slot -> slot > s ^. currentSlot
_ -> True

nextReactiveState slot' = do
end <- viewContractState endSlot
p <- viewContractState phase
when (slot' >= end && p == Bidding) $ do
w <- viewContractState winner
bid <- viewContractState currentBid
phase $= AuctionOver
deposit w theToken
deposit w1 $ Ada.lovelaceValueOf bid

-- This command is only for setting up the model state with theToken
nextState cmd = do
slot <- viewModelState currentSlot
Expand All @@ -221,20 +231,12 @@ instance ContractModel AuctionModel where
Bid w bid -> do
current <- viewContractState currentBid
leader <- viewContractState winner
wait 2
when (bid > current && slot <= end) $ do
when (bid > current && slot < end) $ do
withdraw w $ Ada.lovelaceValueOf bid
deposit leader $ Ada.lovelaceValueOf current
currentBid $= bid
winner $= w
slot' <- viewModelState currentSlot
p <- viewContractState phase
when (slot' > end && p == Bidding) $ do
w <- viewContractState winner
bid <- viewContractState currentBid
phase $= AuctionOver
deposit w theToken
deposit w1 $ Ada.lovelaceValueOf bid
wait 2

perform _ _ Init = delay 3
perform _ _ (WaitUntil slot) = void $ Trace.waitUntilSlot slot
Expand Down