packages feed

quickcheck-lockstep 0.2.1 → 0.3.0

raw patch · 12 files changed

+528/−302 lines, 12 filesdep ~basedep ~mtldep ~quickcheck-dynamicnew-uploader

Dependency ranges changed: base, mtl, quickcheck-dynamic

Files

CHANGELOG.md view
@@ -1,5 +1,10 @@ # Revision history for quickcheck-lockstep +## 0.3.0 -- 2023-10-17++* BREAKING: Update `quickcheck-dynamic` dependency to `>=3.3`.+* Add compatibility with ghc-9.6 (Javier Sagredo)+ ## 0.2.1 -- 2022-12-06  * Expose necessary definitions for custom `Operation` instances (Joris Dral)
quickcheck-lockstep.cabal view
@@ -1,10 +1,10 @@ cabal-version:      2.4 name:               quickcheck-lockstep-version:            0.2.1+version:            0.3.0 license:            BSD-3-Clause license-file:       LICENSE author:             Edsko de Vries-maintainer:         edsko@well-typed.com+maintainer:         edsko@well-typed.com, joris@well-typed.com extra-source-files: CHANGELOG.md category:           Testing synopsis:           Library for lockstep-style testing with 'quickcheck-dynamic'@@ -13,7 +13,7 @@                     APIs calls, then execute them both against the system under                     test and against a model, and compare responses up to some                     notion of observability.-tested-with:        GHC ==8.10.7 || ==9.0.2 || ==9.2.4 || ==9.4.2+tested-with:        GHC ==8.10 || ==9.0 || ==9.2 || ==9.4 || ==9.6  source-repository head   type:     git@@ -59,12 +59,12 @@       Test.QuickCheck.StateModel.Lockstep.GVar   build-depends:       -- quickcheck-dynamic requires ghc 8.10 minimum-      base               >= 4.14 && < 4.18-    , constraints        >= 0.13 && < 0.14-    , mtl                >= 2.2  && < 2.3-    , containers         >= 0.6  && < 0.7-    , QuickCheck         >= 2.14 && < 2.15-    , quickcheck-dynamic >= 2.0  && < 2.1+      base               >= 4.14   && < 4.19+    , constraints        >= 0.13   && < 0.14+    , mtl                >= 2.2    && < 2.4+    , containers         >= 0.6    && < 0.7+    , QuickCheck         >= 2.14   && < 2.15+    , quickcheck-dynamic >= 3.3.1  && < 3.4   hs-source-dirs:       src @@ -80,7 +80,8 @@   other-modules:       Test.MockFS       Test.MockFS.Mock-      Test.IORef+      Test.IORef.Full+      Test.IORef.Simple   default-extensions:       DeriveGeneric       EmptyCase
src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs view
@@ -1,3 +1,5 @@+{-# OPTIONS_GHC -Wno-orphans #-}+ -- | Default implementations for the @quickcheck-dynamic@ class methods -- -- Intended for qualified import.@@ -18,12 +20,14 @@ import Prelude hiding (init)  import Data.Constraint (Dict(..))-import Data.Maybe (isNothing)+import Data.Set qualified as Set import Data.Typeable  import Test.QuickCheck (Gen, Property) import Test.QuickCheck qualified as QC-import Test.QuickCheck.StateModel (Var, Any(..), LookUp, Realized)+import Test.QuickCheck.StateModel ( Var, Any(..), LookUp, Realized, PostconditionM+                                  , Action, monitorPost)+import Test.QuickCheck.StateModel.Variables (VarContext, HasVariables (..))  import Test.QuickCheck.StateModel.Lockstep.API import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)@@ -68,16 +72,17 @@ -- | Default implementation for 'Test.QuickCheck.StateModel.arbitraryAction' arbitraryAction ::      InLockstep state-  => Lockstep state -> Gen (Any (LockstepAction state))-arbitraryAction (Lockstep state env) =+  => VarContext -> Lockstep state -> Gen (Any (LockstepAction state))+arbitraryAction _ (Lockstep state env) =     arbitraryWithVars (varsOfType env) state  -- | Default implementation for 'Test.QuickCheck.StateModel.shrinkAction' shrinkAction ::      InLockstep state-  => Lockstep state+  => VarContext+  -> Lockstep state   -> LockstepAction state a -> [Any (LockstepAction state)]-shrinkAction (Lockstep state env) =+shrinkAction _ (Lockstep state env) =     shrinkWithVars (varsOfType env) state  {-------------------------------------------------------------------------------@@ -94,9 +99,11 @@   -> LockstepAction state a   -> LookUp m   -> Realized m a-  -> m Bool+  -> PostconditionM m Bool postcondition (before, _after) action _lookUp a =-    pure $ isNothing $ checkResponse (Proxy @m) before action a+    case checkResponse (Proxy @m) before action a of+      Nothing -> pure True+      Just s  -> monitorPost (QC.counterexample s) >> pure False  monitoring :: forall m state a.      RunLockstep state m@@ -106,9 +113,8 @@   -> LookUp m   -> Realized m a   -> Property -> Property-monitoring p (before, after) action _lookUp realResp =+monitoring _p (before, after) action _lookUp _realResp =       QC.counterexample ("State: " ++ show after)-    . maybe id QC.counterexample (checkResponse p before action realResp)     . QC.tabulate "Tags" tags   where     tags :: [String]@@ -119,6 +125,24 @@                         action                         (lookUpEnvF $ lockstepEnv before)                         (lockstepModel before)++{-------------------------------------------------------------------------------+  Default class instances+-------------------------------------------------------------------------------}++-- | Ignore variables for lockstep state.+--+-- We largely ignore @quickcheck-dynamic@'s variables in the lockstep framework,+-- since it does its own accounting of model variables.+instance HasVariables (Lockstep state) where+  getAllVariables _ = Set.empty++-- | Ignore variables for lockstep actions.+--+-- We largely ignore @quickcheck-dynamic@'s variables in the lockstep framework,+-- since it does its own accounting of model variables.+instance HasVariables (Action (Lockstep state) a) where+  getAllVariables _ = Set.empty  {-------------------------------------------------------------------------------   Internal auxiliary
src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs view
@@ -21,7 +21,7 @@ import Data.Maybe (mapMaybe) import Data.Typeable -import Test.QuickCheck.StateModel (Var(..))+import Test.QuickCheck.StateModel.Variables (Var, unsafeCoerceVar)  {-------------------------------------------------------------------------------   Types@@ -51,8 +51,8 @@     asum $ map (\(EnvEntry var' fa') -> aux var var' fa') env   where     aux :: Typeable a' => Var a -> Var a' -> f a' -> Maybe (f a)-    aux (Var x) (Var y) fa' = do-        guard (x == y)+    aux v1 v2 fa' = do+        guard (v1 == unsafeCoerceVar v2)         cast fa'  keysOfType :: Typeable a => EnvF f -> [Var a]
src/Test/QuickCheck/StateModel/Lockstep/GVar.hs view
@@ -21,7 +21,7 @@ import Data.Maybe (isJust, fromJust) import Data.Typeable -import Test.QuickCheck.StateModel (Var(..), LookUp, Realized)+import Test.QuickCheck.StateModel (Var, LookUp, Realized)  import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF) import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF
src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs view
@@ -1,5 +1,10 @@+{-# LANGUAGE CPP #-}+ module Test.QuickCheck.StateModel.Lockstep.Op.SumProd (Op(..), intOpId) where +#if __GLASGOW_HASKELL__ >= 906+import Control.Monad ((<=<))+#endif import Control.Monad.Reader (ReaderT) import Control.Monad.State import GHC.Show (appPrec)
src/Test/QuickCheck/StateModel/Lockstep/Run.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ -- | Run lockstep tests -- -- Intended for qualified import.@@ -15,7 +17,11 @@ import Prelude hiding (init)  import Control.Exception+#if __GLASGOW_HASKELL__ >= 906+import Control.Monad (void)+#else import Control.Monad.Reader+#endif import Data.Set (Set) import Data.Set qualified as Set import Data.Typeable@@ -63,7 +69,7 @@   where     go :: Set String -> Lockstep state -> [Step (Lockstep state)] -> [String]     go tags _st []            = Set.toList tags-    go tags  st ((v:=a) : ss) = go' tags st v a ss+    go tags  st ((v:=a) : ss) = go' tags st v (polarAction a) ss      go' :: forall a.          Typeable a
test/Main.hs view
@@ -2,11 +2,13 @@  import Test.Tasty -import Test.IORef qualified-import Test.MockFS qualified+import Test.IORef.Full   qualified+import Test.IORef.Simple qualified+import Test.MockFS       qualified  main :: IO () main = defaultMain $ testGroup "quickcheck-lockstep" [-      Test.IORef.tests+      Test.IORef.Simple.tests+    , Test.IORef.Full.tests     , Test.MockFS.tests     ]
− test/Test/IORef.hs 
@@ -1,273 +0,0 @@-{-# LANGUAGE RecordWildCards #-}--{-# OPTIONS_GHC -Wno-orphans #-}--module Test.IORef (tests) where--import Control.Monad.Reader-import Data.Bifunctor-import Data.Constraint (Dict(..))-import Data.IORef-import Data.Map (Map)-import Data.Map qualified as Map-import Data.Proxy-import Test.QuickCheck-import Test.Tasty-import Test.Tasty.HUnit-import Test.Tasty.QuickCheck (testProperty)--import Test.QuickCheck qualified as QC--import Test.QuickCheck.StateModel-import Test.QuickCheck.StateModel.Lockstep-import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep-import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep-import Test.QuickCheck.StateModel.Lockstep.Run (labelActions)--{--------------------------------------------------------------------------------  Model "M"--------------------------------------------------------------------------------}--type MRef = Int--data M = M {-      -- | Value of every var-      mValues :: Map MRef Int--      -- | Often did we write each value to each var?-      ---      -- This is used for tagging.-    , mWrites :: Map (MRef, Int) Int-    }-  deriving (Show)--initModel :: M-initModel = M {-      mValues = Map.empty-    , mWrites = Map.empty-    }--modelNew :: M -> (MRef, M)-modelNew M{..} = (-      mockRef-    , M { mValues = Map.insert mockRef 0 mValues-        , mWrites = mWrites-        }-    )-  where-    mockRef :: MRef-    mockRef = Map.size mValues--modelWrite :: MRef -> Int -> M -> (Int, M)-modelWrite v x M{..} = (-      x-    , M { mValues = Map.insert v x mValues-        , mWrites = Map.alter recordWrite (v, x) mWrites-        }-    )-  where-    recordWrite :: Maybe Int -> Maybe Int-    recordWrite Nothing  = Just 1 -- First write-    recordWrite (Just n) = Just (n + 1)--modelRead :: MRef -> M -> (Int, M)-modelRead v m@M{..} = (mValues Map.! v, m)--{--------------------------------------------------------------------------------  Instances--------------------------------------------------------------------------------}--instance StateModel (Lockstep M) where-  data Action (Lockstep M) a where-    -- | Create new IORef-    New :: Action (Lockstep M) (IORef Int)--    -- | Write value to IORef-    ---    -- The value is specified either as a concrete value or by reference-    -- to a previous write.-    Write ::-         ModelVar M (IORef Int)-      -> Either Int (ModelVar M Int)-      -> Action (Lockstep M) Int--    -- | Read IORef-    Read ::-         ModelVar M (IORef Int)-      -> Action (Lockstep M) Int--  initialState    = Lockstep.initialState initModel-  nextState       = Lockstep.nextState-  precondition    = Lockstep.precondition-  arbitraryAction = Lockstep.arbitraryAction-  shrinkAction    = Lockstep.shrinkAction--instance RunModel (Lockstep M) RealMonad where-  perform       = \_state -> runIO-  postcondition = Lockstep.postcondition-  monitoring    = Lockstep.monitoring (Proxy @RealMonad)--instance InLockstep M where-  data ModelValue M a where-    MRef  :: MRef -> ModelValue M (IORef Int)-    MInt  :: Int  -> ModelValue M Int--  data Observable M a where-    ORef :: Observable M (IORef Int)-    OId  :: (Show a, Eq a) => a -> Observable M a--  observeModel (MRef  _) = ORef-  observeModel (MInt  x) = OId x--  usedVars New                  = []-  usedVars (Write v (Left _))   = [SomeGVar v]-  usedVars (Write v (Right v')) = [SomeGVar v, SomeGVar v']-  usedVars (Read  v)            = [SomeGVar v]--  modelNextState = runModel--  arbitraryWithVars findVars _mock = oneof $ concat [-        withoutVars-      , case findVars (Proxy @(IORef Int)) of-          []   -> []-          vars -> withVars (elements vars)-      ]-    where-      withoutVars :: [Gen (Any (LockstepAction M))]-      withoutVars = [return $ Some New]--      withVars ::-           Gen (ModelVar M (IORef Int))-        -> [Gen (Any (LockstepAction M))]-      withVars genVar = [-            fmap Some $ Write <$> genVar <*> (Left <$> choose (0, 10))-          , fmap Some $ Read  <$> genVar-          ]--  shrinkWithVars findVars _mock = \case-      New               -> []-      Write v (Left x)  -> concat [-                               Some . Write v . Left  <$> shrink x-                             , Some . Write v . Right <$> findVars (Proxy @Int)-                             ]-      Write _ (Right _) -> []-      Read  _           -> []--  tagStep (_stBefore, stAfter) _action _result = concat [-        [ "WriteSameVarTwice"-        | not-        . Map.null-        . Map.filter (\numWrites -> numWrites > 1)-        $ mWrites stAfter-        ]-      ]--instance RunLockstep M RealMonad where-  observeReal _ action result =-      case (action, result) of-        (New     , _) -> ORef-        (Write{} , x) -> OId x-        (Read{}  , x) -> OId x--  showRealResponse _ = \case-    New{}   -> Nothing-    Write{} -> Just Dict-    Read{}  -> Just Dict--deriving instance Show (Action (Lockstep M) a)-deriving instance Show (Observable M a)-deriving instance Show (ModelValue M a)--deriving instance Eq (Action (Lockstep M) a)-deriving instance Eq (Observable M a)-deriving instance Eq (ModelValue M a)--{--------------------------------------------------------------------------------  Interpreters against the real system and against the model--------------------------------------------------------------------------------}--data Buggy = Buggy | NotBuggy-  deriving (Show, Eq)--instance Arbitrary Buggy where-  arbitrary = elements [Buggy, NotBuggy]--  shrink Buggy    = [NotBuggy]-  shrink NotBuggy = []---- | We trigger a bug if we write the /same/ value to the /same/ variable-type BrokenRef = [(IORef Int, Int)]--type RealMonad = ReaderT (Buggy, IORef BrokenRef) IO--runIO :: Action (Lockstep M) a -> LookUp RealMonad -> RealMonad a-runIO action lookUp = ReaderT $ \(buggy, brokenRef) ->-    case action of-      New       -> newIORef 0-      Write v x -> brokenWrite buggy brokenRef (lookUpRef v) (lookUpInt x)-      Read  v   -> readIORef (lookUpRef v)-  where-    lookUpRef :: ModelVar M (IORef Int) -> IORef Int-    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp--    lookUpInt :: Either Int (ModelVar M Int) -> Int-    lookUpInt (Left  x) = x-    lookUpInt (Right v) = lookUpGVar (Proxy @RealMonad) lookUp v---- | The second write to the same variable will be broken-brokenWrite :: Buggy -> IORef BrokenRef -> IORef Int -> Int -> IO Int-brokenWrite NotBuggy _         v x = writeIORef v x >> return x-brokenWrite Buggy    brokenRef v x = do-    broken <- readIORef brokenRef-    if (v, x) `elem` broken then-      writeIORef v 123456789-    else-      writeIORef v x-    modifyIORef brokenRef ((v, x) :)-    return x--runModel ::-     Action (Lockstep M) a-  -> ModelLookUp M-  -> M -> (ModelValue M a, M)-runModel action lookUp =-    case action of-      New       -> first MRef . modelNew-      Write v x -> first MInt . modelWrite (lookUpRef v) (lookUpInt x)-      Read  v   -> first MInt . modelRead  (lookUpRef v)-  where-    lookUpRef :: ModelVar M (IORef Int) -> MRef-    lookUpRef var = case lookUp var of MRef r -> r--    lookUpInt :: Either Int (ModelVar M Int) -> Int-    lookUpInt (Left  x) = x-    lookUpInt (Right v) = case lookUp v of MInt x -> x--{--------------------------------------------------------------------------------  Top-level tests--------------------------------------------------------------------------------}--propIORef :: Buggy -> Actions (Lockstep M) -> Property-propIORef buggy actions =-      (if triggersBug then expectFailure  else id)-    $ Lockstep.runActionsBracket-        (Proxy @M)-        initBroken-        (\_ -> return ())-        runReaderT-        actions-  where-    triggersBug :: Bool-    triggersBug =-           buggy == Buggy-        && "WriteSameVarTwice" `elem` labelActions actions--    initBroken :: IO (Buggy, IORef BrokenRef)-    initBroken = (buggy,) <$> newIORef []--tests :: TestTree-tests = testGroup "Test.IORef" [-      testCase "labelledExamples" $-        QC.labelledExamples $ Lockstep.tagActions (Proxy @M)-    , testProperty "runActions" propIORef-    ]
+ test/Test/IORef/Full.hs view
@@ -0,0 +1,273 @@+{-# LANGUAGE RecordWildCards #-}++{-# OPTIONS_GHC -Wno-orphans #-}++module Test.IORef.Full (tests) where++import Control.Monad.Reader+import Data.Bifunctor+import Data.Constraint (Dict(..))+import Data.IORef+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Proxy+import Test.QuickCheck+import Test.Tasty+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck (testProperty)++import Test.QuickCheck qualified as QC++import Test.QuickCheck.StateModel+import Test.QuickCheck.StateModel.Lockstep+import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep+import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep+import Test.QuickCheck.StateModel.Lockstep.Run (labelActions)++{-------------------------------------------------------------------------------+  Model "M"+-------------------------------------------------------------------------------}++type MRef = Int++data M = M {+      -- | Value of every var+      mValues :: Map MRef Int++      -- | Often did we write each value to each var?+      --+      -- This is used for tagging.+    , mWrites :: Map (MRef, Int) Int+    }+  deriving (Show)++initModel :: M+initModel = M {+      mValues = Map.empty+    , mWrites = Map.empty+    }++modelNew :: M -> (MRef, M)+modelNew M{..} = (+      mockRef+    , M { mValues = Map.insert mockRef 0 mValues+        , mWrites = mWrites+        }+    )+  where+    mockRef :: MRef+    mockRef = Map.size mValues++modelWrite :: MRef -> Int -> M -> (Int, M)+modelWrite v x M{..} = (+      x+    , M { mValues = Map.insert v x mValues+        , mWrites = Map.alter recordWrite (v, x) mWrites+        }+    )+  where+    recordWrite :: Maybe Int -> Maybe Int+    recordWrite Nothing  = Just 1 -- First write+    recordWrite (Just n) = Just (n + 1)++modelRead :: MRef -> M -> (Int, M)+modelRead v m@M{..} = (mValues Map.! v, m)++{-------------------------------------------------------------------------------+  Instances+-------------------------------------------------------------------------------}++instance StateModel (Lockstep M) where+  data Action (Lockstep M) a where+    -- | Create new IORef+    New :: Action (Lockstep M) (IORef Int)++    -- | Write value to IORef+    --+    -- The value is specified either as a concrete value or by reference+    -- to a previous write.+    Write ::+         ModelVar M (IORef Int)+      -> Either Int (ModelVar M Int)+      -> Action (Lockstep M) Int++    -- | Read IORef+    Read ::+         ModelVar M (IORef Int)+      -> Action (Lockstep M) Int++  initialState    = Lockstep.initialState initModel+  nextState       = Lockstep.nextState+  precondition    = Lockstep.precondition+  arbitraryAction = Lockstep.arbitraryAction+  shrinkAction    = Lockstep.shrinkAction++instance RunModel (Lockstep M) RealMonad where+  perform       = \_state -> runIO+  postcondition = Lockstep.postcondition+  monitoring    = Lockstep.monitoring (Proxy @RealMonad)++instance InLockstep M where+  data ModelValue M a where+    MRef  :: MRef -> ModelValue M (IORef Int)+    MInt  :: Int  -> ModelValue M Int++  data Observable M a where+    ORef :: Observable M (IORef Int)+    OId  :: (Show a, Eq a) => a -> Observable M a++  observeModel (MRef  _) = ORef+  observeModel (MInt  x) = OId x++  usedVars New                  = []+  usedVars (Write v (Left _))   = [SomeGVar v]+  usedVars (Write v (Right v')) = [SomeGVar v, SomeGVar v']+  usedVars (Read  v)            = [SomeGVar v]++  modelNextState = runModel++  arbitraryWithVars findVars _mock = oneof $ concat [+        withoutVars+      , case findVars (Proxy @(IORef Int)) of+          []   -> []+          vars -> withVars (elements vars)+      ]+    where+      withoutVars :: [Gen (Any (LockstepAction M))]+      withoutVars = [return $ Some New]++      withVars ::+           Gen (ModelVar M (IORef Int))+        -> [Gen (Any (LockstepAction M))]+      withVars genVar = [+            fmap Some $ Write <$> genVar <*> (Left <$> choose (0, 10))+          , fmap Some $ Read  <$> genVar+          ]++  shrinkWithVars findVars _mock = \case+      New               -> []+      Write v (Left x)  -> concat [+                               Some . Write v . Left  <$> shrink x+                             , Some . Write v . Right <$> findVars (Proxy @Int)+                             ]+      Write _ (Right _) -> []+      Read  _           -> []++  tagStep (_stBefore, stAfter) _action _result = concat [+        [ "WriteSameVarTwice"+        | not+        . Map.null+        . Map.filter (\numWrites -> numWrites > 1)+        $ mWrites stAfter+        ]+      ]++instance RunLockstep M RealMonad where+  observeReal _ action result =+      case (action, result) of+        (New     , _) -> ORef+        (Write{} , x) -> OId x+        (Read{}  , x) -> OId x++  showRealResponse _ = \case+    New{}   -> Nothing+    Write{} -> Just Dict+    Read{}  -> Just Dict++deriving instance Show (Action (Lockstep M) a)+deriving instance Show (Observable M a)+deriving instance Show (ModelValue M a)++deriving instance Eq (Action (Lockstep M) a)+deriving instance Eq (Observable M a)+deriving instance Eq (ModelValue M a)++{-------------------------------------------------------------------------------+  Interpreters against the real system and against the model+-------------------------------------------------------------------------------}++data Buggy = Buggy | NotBuggy+  deriving (Show, Eq)++instance Arbitrary Buggy where+  arbitrary = elements [Buggy, NotBuggy]++  shrink Buggy    = [NotBuggy]+  shrink NotBuggy = []++-- | We trigger a bug if we write the /same/ value to the /same/ variable+type BrokenRef = [(IORef Int, Int)]++type RealMonad = ReaderT (Buggy, IORef BrokenRef) IO++runIO :: Action (Lockstep M) a -> LookUp RealMonad -> RealMonad a+runIO action lookUp = ReaderT $ \(buggy, brokenRef) ->+    case action of+      New       -> newIORef 0+      Write v x -> brokenWrite buggy brokenRef (lookUpRef v) (lookUpInt x)+      Read  v   -> readIORef (lookUpRef v)+  where+    lookUpRef :: ModelVar M (IORef Int) -> IORef Int+    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp++    lookUpInt :: Either Int (ModelVar M Int) -> Int+    lookUpInt (Left  x) = x+    lookUpInt (Right v) = lookUpGVar (Proxy @RealMonad) lookUp v++-- | The second write to the same variable will be broken+brokenWrite :: Buggy -> IORef BrokenRef -> IORef Int -> Int -> IO Int+brokenWrite NotBuggy _         v x = writeIORef v x >> return x+brokenWrite Buggy    brokenRef v x = do+    broken <- readIORef brokenRef+    if (v, x) `elem` broken then+      writeIORef v 123456789+    else+      writeIORef v x+    modifyIORef brokenRef ((v, x) :)+    return x++runModel ::+     Action (Lockstep M) a+  -> ModelLookUp M+  -> M -> (ModelValue M a, M)+runModel action lookUp =+    case action of+      New       -> first MRef . modelNew+      Write v x -> first MInt . modelWrite (lookUpRef v) (lookUpInt x)+      Read  v   -> first MInt . modelRead  (lookUpRef v)+  where+    lookUpRef :: ModelVar M (IORef Int) -> MRef+    lookUpRef var = case lookUp var of MRef r -> r++    lookUpInt :: Either Int (ModelVar M Int) -> Int+    lookUpInt (Left  x) = x+    lookUpInt (Right v) = case lookUp v of MInt x -> x++{-------------------------------------------------------------------------------+  Top-level tests+-------------------------------------------------------------------------------}++propIORef :: Buggy -> Actions (Lockstep M) -> Property+propIORef buggy actions =+      (if triggersBug then expectFailure  else id)+    $ Lockstep.runActionsBracket+        (Proxy @M)+        initBroken+        (\_ -> return ())+        runReaderT+        actions+  where+    triggersBug :: Bool+    triggersBug =+           buggy == Buggy+        && "WriteSameVarTwice" `elem` labelActions actions++    initBroken :: IO (Buggy, IORef BrokenRef)+    initBroken = (buggy,) <$> newIORef []++tests :: TestTree+tests = testGroup "Test.IORef.Full" [+      testCase "labelledExamples" $+        QC.labelledExamples $ Lockstep.tagActions (Proxy @M)+    , testProperty "runActions" propIORef+    ]
+ test/Test/IORef/Simple.hs view
@@ -0,0 +1,183 @@+{-# LANGUAGE RecordWildCards #-}++{-# OPTIONS_GHC -Wno-orphans #-}++module Test.IORef.Simple (tests) where++import Data.Bifunctor+import Data.Constraint (Dict(..))+import Data.IORef+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Proxy+import Test.QuickCheck+import Test.Tasty+import Test.Tasty.QuickCheck (testProperty)++import Test.QuickCheck.StateModel+import Test.QuickCheck.StateModel.Lockstep+import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep+import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep++{-------------------------------------------------------------------------------+  Model "M"+-------------------------------------------------------------------------------}++type MRef = Int++data M = M {+      -- | Value of every var+      mValues :: Map MRef Int+    }+  deriving (Show)++initModel :: M+initModel = M { mValues = Map.empty }++modelNew :: M -> (MRef, M)+modelNew M{..} = (+      mockRef+    , M { mValues = Map.insert mockRef 0 mValues }+    )+  where+    mockRef :: MRef+    mockRef = Map.size mValues++modelWrite :: MRef -> Int -> M -> ((), M)+modelWrite v x M{..} = (+      ()+    , M { mValues = Map.insert v x mValues }+    )++modelRead :: MRef -> M -> (Int, M)+modelRead v m@M{..} = (mValues Map.! v, m)++{-------------------------------------------------------------------------------+  Instances+-------------------------------------------------------------------------------}++instance StateModel (Lockstep M) where+  data Action (Lockstep M) a where+    -- | Create new IORef+    New :: Action (Lockstep M) (IORef Int)++    -- | Write value to IORef+    Write ::+         ModelVar M (IORef Int)+      -> Int+      -> Action (Lockstep M) ()++    -- | Read IORef+    Read ::+         ModelVar M (IORef Int)+      -> Action (Lockstep M) Int++  initialState    = Lockstep.initialState initModel+  nextState       = Lockstep.nextState+  precondition    = Lockstep.precondition+  arbitraryAction = Lockstep.arbitraryAction+  shrinkAction    = Lockstep.shrinkAction++instance RunModel (Lockstep M) RealMonad where+  perform       = \_state -> runIO+  postcondition = Lockstep.postcondition+  monitoring    = Lockstep.monitoring (Proxy @RealMonad)++instance InLockstep M where+  data ModelValue M a where+    MRef  :: MRef -> ModelValue M (IORef Int)+    MUnit :: ()   -> ModelValue M ()+    MInt  :: Int  -> ModelValue M Int++  data Observable M a where+    ORef :: Observable M (IORef Int)+    OId  :: (Show a, Eq a) => a -> Observable M a++  observeModel (MRef  _) = ORef+  observeModel (MUnit x) = OId x+  observeModel (MInt  x) = OId x++  usedVars New         = []+  usedVars (Write v _) = [SomeGVar v]+  usedVars (Read  v)   = [SomeGVar v]++  modelNextState = runModel++  arbitraryWithVars findVars _mock = oneof $ concat [+        withoutVars+      , case findVars (Proxy @(IORef Int)) of+          []   -> []+          vars -> withVars (elements vars)+      ]+    where+      withoutVars :: [Gen (Any (LockstepAction M))]+      withoutVars = [return $ Some New]++      withVars ::+           Gen (ModelVar M (IORef Int))+        -> [Gen (Any (LockstepAction M))]+      withVars genVar = [+            fmap Some $ Write <$> genVar <*> choose (0, 10)+          , fmap Some $ Read  <$> genVar+          ]++instance RunLockstep M RealMonad where+  observeReal _ action result =+      case (action, result) of+        (New     , _) -> ORef+        (Write{} , x) -> OId x+        (Read{}  , x) -> OId x++  showRealResponse _ = \case+    New{}   -> Nothing+    Write{} -> Just Dict+    Read{}  -> Just Dict++deriving instance Show (Action (Lockstep M) a)+deriving instance Show (Observable M a)+deriving instance Show (ModelValue M a)++deriving instance Eq (Action (Lockstep M) a)+deriving instance Eq (Observable M a)+deriving instance Eq (ModelValue M a)++{-------------------------------------------------------------------------------+  Interpreters against the real system and against the model+-------------------------------------------------------------------------------}++type RealMonad = IO++runIO :: Action (Lockstep M) a -> LookUp RealMonad -> RealMonad a+runIO action lookUp =+    case action of+      New       -> newIORef 0+      Write v x -> writeIORef (lookUpRef v) x+      Read  v   -> readIORef (lookUpRef v)+  where+    lookUpRef :: ModelVar M (IORef Int) -> IORef Int+    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp++runModel ::+     Action (Lockstep M) a+  -> ModelLookUp M+  -> M -> (ModelValue M a, M)+runModel action lookUp =+    case action of+      New       -> first MRef  . modelNew+      Write v x -> first MUnit . modelWrite (lookUpRef v) x+      Read  v   -> first MInt  . modelRead  (lookUpRef v)+  where+    lookUpRef :: ModelVar M (IORef Int) -> MRef+    lookUpRef var = case lookUp var of MRef r -> r++{-------------------------------------------------------------------------------+  Top-level tests+-------------------------------------------------------------------------------}++propIORef :: Actions (Lockstep M) -> Property+propIORef = Lockstep.runActions (Proxy @M)++tests :: TestTree+tests = testGroup "Test.IORef.Simple" [+      testProperty "runActions" propIORef+    ]
test/Test/MockFS.hs view
@@ -32,7 +32,7 @@  import Test.QuickCheck (Gen) import Test.QuickCheck qualified as QC-import Test.QuickCheck.StateModel+import Test.QuickCheck.StateModel hiding (vars)  import Test.QuickCheck.StateModel.Lockstep import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep