-
-
Save thumphries/2e68275819e05a0d5e27ecb5dcd85dce to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- https://en.wikipedia.org/wiki/Finite-state_machine#/media/File:Turnstile_state_machine_colored.svg | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE OverloadedStrings #-} | |
{-# LANGUAGE TemplateHaskell #-} | |
module Test.Example.Turnstile where | |
import Control.Monad | |
import Control.Monad.IO.Class (MonadIO (..)) | |
import Data.IORef | |
import Hedgehog | |
import qualified Hedgehog.Gen as Gen | |
import qualified Hedgehog.Range as Range | |
data TurnstileState = | |
Locked | |
| Unlocked | |
deriving (Eq, Ord, Show) | |
newtype Turnstile = Turnstile { | |
unTurnstile :: IORef TurnstileState | |
} | |
newTurnstile :: IO Turnstile | |
newTurnstile = | |
Turnstile <$> newIORef Locked | |
turnstileState :: Turnstile -> IO TurnstileState | |
turnstileState = | |
readIORef . unTurnstile | |
insertCoin :: Turnstile -> IO () | |
insertCoin (Turnstile ref) = | |
atomicModifyIORef' ref $ \_ -> | |
(Unlocked, ()) | |
pushTurnstile :: Turnstile -> IO Bool | |
pushTurnstile (Turnstile ref) = | |
atomicModifyIORef' ref $ \s -> | |
case s of | |
Locked -> | |
(Locked, False) | |
Unlocked -> | |
(Locked, True) | |
-------------------------------------------------------------------------------- | |
data ModelState (v :: * -> *) = | |
TLocked | |
| TUnlocked | |
deriving (Eq, Ord, Show) | |
initialState :: ModelState v | |
initialState = | |
TLocked | |
-------------------------------------------------------------------------------- | |
data Coin (v :: * -> *) = | |
Coin | |
deriving (Eq, Show) | |
instance HTraversable Coin where | |
htraverse _ Coin = | |
pure Coin | |
s_coin :: (Monad n, MonadIO m, MonadTest m) => Turnstile -> Command n m ModelState | |
s_coin ts = | |
let | |
-- We can always insert a coin, so we don't need to see the state. | |
gen _state = | |
Just $ | |
pure Coin | |
-- We execute this action by calling 'insertCoin'. | |
execute Coin = | |
liftIO (insertCoin ts) | |
in | |
Command gen execute [ | |
-- After a coin action, the turnstile should be unlocked. | |
-- First we update our model: | |
Update $ \s Coin _o -> | |
TUnlocked | |
-- ... then we enforce a very simple predicate on it: | |
, Ensure $ \_before after Coin () -> do | |
after === TUnlocked | |
] | |
-------------------------------------------------------------------------------- | |
data Push (v :: * -> *) = | |
Push | |
deriving (Eq, Show) | |
instance HTraversable Push where | |
htraverse _ Push = | |
pure Push | |
s_push_locked :: (Monad n, MonadIO m, MonadTest m) => Turnstile -> Command n m ModelState | |
s_push_locked ts = | |
let | |
-- This generator only succeeds when the gate is thought to be locked. | |
gen state = | |
case state of | |
TLocked -> | |
Just $ | |
pure Push | |
TUnlocked -> | |
Nothing | |
execute Push = do | |
liftIO $ pushTurnstile ts | |
in | |
Command gen execute [ | |
-- Precondition: the gate is thought to be locked. | |
Require $ \s Push -> | |
s == TLocked | |
-- Update: pushing the locked gate has no effect. | |
, Update $ \s Push _o -> | |
TLocked | |
-- Postcondition: we're denied admission, the turnstile gate stays locked. | |
, Ensure $ \before after Push b -> do | |
before === TLocked | |
assert (not b) | |
after === TLocked | |
] | |
s_push_unlocked :: (Monad n, MonadIO m, MonadTest m) => Turnstile -> Command n m ModelState | |
s_push_unlocked ts = | |
let | |
gen state = | |
case state of | |
TUnlocked -> | |
Just $ | |
pure Push | |
TLocked -> | |
Nothing | |
execute Push = do | |
liftIO $ pushTurnstile ts | |
in | |
Command gen execute [ | |
-- Precondition: the gate is thought to be unlocked. | |
Require $ \s Push -> | |
s == TUnlocked | |
-- Update: pushing the unlocked gate locks it. | |
, Update $ \s Push _o -> | |
TLocked | |
-- Postcondition: we gain admission, the turnstile gate is locked. | |
, Ensure $ \before after Push b -> do | |
before === TUnlocked | |
assert b | |
after === TLocked | |
] | |
-------------------------------------------------------------------------------- | |
prop_turnstile :: Property | |
prop_turnstile = | |
property $ do | |
turnstile <- liftIO newTurnstile | |
actions <- forAll $ | |
Gen.actions (Range.linear 1 100) initialState [ | |
s_coin turnstile | |
, s_push_locked turnstile | |
, s_push_unlocked turnstile | |
] | |
executeSequential initialState actions | |
-------------------------------------------------------------------------------- | |
return [] | |
tests :: IO Bool | |
tests = | |
checkParallel $$(discover) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Thanks for your great blogpost! In case anybody else stumbles upon this, I think line 163 should be
Gen.sequential
instead ofGen.actions
(maybe that changed in hedgehog).EDIT: Yes it did change with the parallel state machine stuff.