Create a gist now

Instantly share code, notes, and snippets.

@thumphries /turnstile.hs Secret
Last active Aug 6, 2017

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 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