Skip to content

Instantly share code, notes, and snippets.

@thumphries thumphries/turnstile.hs Secret
Last active Jan 26, 2019

Embed
What would you like to do?
-- 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)
@cocreature

This comment has been minimized.

Copy link

cocreature commented Jul 16, 2017

Thanks for your great blogpost! In case anybody else stumbles upon this, I think line 163 should be Gen.sequential instead of Gen.actions (maybe that changed in hedgehog).
EDIT: Yes it did change with the parallel state machine stuff.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.