An attempt at better documentation for q-d

cabal.project

@@ -1,6 +1,7 @@
 packages:
   quickcheck-dynamic
   quickcheck-dynamic-iosim
+  docs
 
 tests: true
 

docs/CircularBuffer/Buffer.lhs

@@ -0,0 +1,66 @@
+> {-# LANGUAGE NamedFieldPuns #-}
+
+> -- | A Reasonably efficient version of a ring buffer.
+> -- Directly stolen from [q-s-m](https://github.com/stevana/quickcheck-state-machine/blob/master/test/CircularBuffer.hs#L86)
+> module CircularBuffer.Buffer where
+
+> import Data.Function (on)
+> import Data.IORef (IORef, newIORef, readIORef, writeIORef)
+> import Data.Vector.Unboxed.Mutable (
+>   IOVector,
+>  )
+> import Data.Vector.Unboxed.Mutable qualified as V
+
+> -- | An efficient mutable circular buffer.
+> data Buffer = Buffer
+>   { size :: Int
+>   -- ^ Size of buffer
+>   , inp :: IORef Int
+>   -- ^ Index to the next free slot where to 'Put' the next element
+>   , outp :: IORef Int
+>   -- ^ Index to the last occupied slot to 'Get' an element from
+>   , buf :: IOVector Int
+>   -- ^ Array of elements of fixed capacity
+>   }
+
+> -- | Different buffers are assumed to have disjoint memories,
+> -- so we can use 'V.overlaps' to check equality.
+> instance Eq Buffer where
+>   (==) =
+>     ((==) `on` inp)
+>       `also` ((==) `on` outp)
+>       `also` (V.overlaps `on` buf)
+>     where
+>       also = (liftA2 . liftA2) (&&)
+
+> -- | See 'New'.
+> newBuffer :: Int -> IO Buffer
+> newBuffer n =
+>   Buffer size
+>     <$> newIORef 0
+>     <*> newIORef 0
+>     <*> V.new size
+>   where
+>     size = n + 1
+
+> -- | See 'Put'.
+> putBuffer :: Int -> Buffer -> IO ()
+> putBuffer x Buffer{size, inp, buf} = do
+>   i <- readIORef inp
+>   V.write buf i x
+>   writeIORef inp $! (i + 1) `mod` size
+
+> -- | See 'Get'.
+> getBuffer :: Buffer -> IO Int
+> getBuffer Buffer{size, outp, buf} = do
+>   j <- readIORef outp
+>   y <- V.read buf j
+>   writeIORef outp $! (j + 1) `mod` size
+>   return y
+
+> -- | See 'Len'.
+> lenBuffer :: Buffer -> IO Int
+> lenBuffer Buffer{inp, outp, size} = do
+>   i <- readIORef inp
+>   j <- readIORef outp
+>   pure $ (i - j + size) `rem` size

docs/CircularBuffer/Model.lhs

@@ -0,0 +1,108 @@
+> {-# LANGUAGE InstanceSigs #-}
+> {-# LANGUAGE NamedFieldPuns #-}
+> {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+
+> -- | An classic example of model-checking an implementation of a ring buffer.
+> --
+> -- * Inspired by [q-s-m example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/CircularBuffer.hs)
+> -- * Also described by John Hughes [here](https://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf)
+> module CircularBuffer.Model where
+
+> import Control.Monad.State (MonadState (..), StateT)
+> import Control.Monad.Trans (lift)
+> import Data.Maybe (fromJust)
+> import GHC.Generics (Generic)
+> import CircularBuffer.Buffer (Buffer, getBuffer, lenBuffer, newBuffer, putBuffer)
+> import Test.QuickCheck (Arbitrary (..), Property, getPositive, oneof)
+> import Test.QuickCheck.DynamicLogic (DL, DynLogicModel (..), action, forAllDL)
+> import Test.QuickCheck.Extras (runPropertyStateT)
+> import Test.QuickCheck.Monadic (monadicIO)
+> import Test.QuickCheck.Monadic qualified as QC
+> import Test.QuickCheck.StateModel (Actions, Any (..), HasVariables (..), RunModel (..), StateModel (..), Var, counterexamplePost, runActions)
+
+> -- * Model
+
+> -- | A simple model of a `CircularBuffer` implemented using a `List`.
+> data CircularBufferModel
+>   = NoBuffer
+>   | CircularBufferModel
+>       { size :: Int
+>       , buffer :: [Var Int]
+>       }
+>   deriving (Eq, Show, Generic)
+
+> instance StateModel CircularBufferModel where
+>   data Action CircularBufferModel a where
+>     -- Create new buffer of given capacity.
+>     New :: Int -> Action CircularBufferModel ()
+>     -- Put an element at the top of the buffer.
+>     Put :: Int -> Action CircularBufferModel Int
+>     -- Get an element out of the bottom of the buffer.
+>     Get :: Action CircularBufferModel Int
+>     -- Get the number of elements in the buffer.
+>     Len :: Action CircularBufferModel Int
+
+>   arbitraryAction ctx NoBuffer = Some . New . getPositive <$> arbitrary
+>   arbitraryAction ctx CircularBufferModel{} =
+>     oneof
+>       [ Some . Put <$> arbitrary
+>       , pure $ Some Get
+>       , pure $ Some Len
+>       ]
+
+>   initialState = NoBuffer
+
+>   precondition NoBuffer New{} = True
+>   precondition CircularBufferModel{buffer} Get{} = length buffer > 0
+>   precondition CircularBufferModel{buffer, size} Put{} = length buffer < size
+>   precondition CircularBufferModel{} Len{} = True
+>   precondition _ _ = False
+
+>   nextState NoBuffer (New size) var = CircularBufferModel{size, buffer = mempty}
+>   nextState buf@CircularBufferModel{size, buffer} Put{} var = buf{buffer = var : buffer}
+>   nextState buf@CircularBufferModel{buffer} Get _ = buf{buffer = init buffer}
+>   nextState st _ _ = st
+
+>   shrinkAction _ _ = \case
+>     New n -> Some . New <$> [i | i <- shrink n, i > 0]
+>     Put n -> Some . Put <$> shrink n
+>     _ -> []
+
+> deriving instance Show (Action CircularBufferModel a)
+> deriving instance Eq (Action CircularBufferModel a)
+
+> instance HasVariables (Action CircularBufferModel a) where
+>   getAllVariables = const mempty
+
+> instance DynLogicModel CircularBufferModel where
+>   restricted _ = False
+
+> -- * RunModel
+
+> instance RunModel CircularBufferModel (StateT (Maybe Buffer) IO) where
+>   perform _st action _lookup =
+>     case action of
+>       New n -> lift (newBuffer n) >>= put . Just
+>       Put v -> get >>= (lift . putBuffer v . fromJust) >> pure v
+>       Get -> get >>= lift . getBuffer . fromJust
+>       Len -> get >>= lift . lenBuffer . fromJust
+
+>   postcondition (CircularBufferModel{buffer}, after) Get lookup res =
+>     let v = lookup (last buffer)
+>      in do
+>           counterexamplePost ("Expected: " <> show v <> ", got: " <> show res)
+>           pure $ v == res
+>   postcondition (CircularBufferModel{buffer}, after) Len lookup res = do
+>     let len = length buffer
+>     counterexamplePost $ "Expected; " <> show len <> ", got: " <> show res
+>     pure $ res == len
+>   postcondition _ _ _ _ = pure True
+
+> prop_CircularBuffer :: Actions CircularBufferModel -> Property
+> prop_CircularBuffer s =
+>   monadicIO $ do
+>     runPropertyStateT (runActions @_ @(StateT (Maybe Buffer) IO) s) Nothing
+>     QC.assert True
+
+> propDL :: DL CircularBufferModel () -> Property
+> propDL d = forAllDL d prop_CircularBuffer