Merge pull request #26 from well-typed/jdral/monitor-all-responses

Print all responses in counterexamples

.gitattributes

@@ -0,0 +1 @@
+*.golden	-text

.gitignore

@@ -1,5 +1,7 @@
 dist-newstyle
 .envrc
+_tmp
+haddocks/
 
 # Haskell.gitignore
 dist

CHANGELOG.md

@@ -1,5 +1,15 @@
 # Revision history for quickcheck-lockstep
 
+## ?.?.? -- ????-??-??
+
+* BREAKING: Enable verbose counterexamples by default in the 'postcondition'
+  function using 'postconditionWith'.
+* NON-BREAKING: Add a new 'postconditionWith' function that can be configured to
+  produce more verbose counterexamples. With verbosity disabled, all states of
+  the model are printed in a counterexample. If verbosity is enabled, the
+  counterexample will also include all responses from the real system and the
+  model.
+
 ## 0.6.0 -- 2024-12-03
 
 * BREAKING: Generalise `ModelFindVariables` and `ModelLookup` to

quickcheck-lockstep.cabal

@@ -80,6 +80,7 @@ test-suite test-quickcheck-lockstep
   hs-source-dirs:     test
   main-is:            Main.hs
   other-modules:
+    Test.Golden
     Test.IORef.Full
     Test.IORef.Simple
     Test.MockFS
@@ -101,6 +102,7 @@ test-suite test-quickcheck-lockstep
     , quickcheck-dynamic
     , quickcheck-lockstep
     , tasty
+    , tasty-golden
     , tasty-hunit
     , tasty-quickcheck
     , temporary

src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs

@@ -14,6 +14,7 @@ module Test.QuickCheck.StateModel.Lockstep.Defaults (
   , shrinkAction
     -- * Default implementations for methods of 'RunModel'
   , postcondition
+  , postconditionWith
   , monitoring
   ) where
 
@@ -99,10 +100,27 @@ postcondition :: forall m state a.
   -> LookUp m
   -> Realized m a
   -> PostconditionM m Bool
-postcondition (before, _after) action _lookUp a =
+postcondition = postconditionWith True
+
+-- | Like 'postcondition', but with configurable verbosity.
+--
+-- By default, all states of the model are printed when a property
+-- counterexample is printed. If verbose output is enabled, the counterexample
+-- will also print all responses from the real system and the model.
+postconditionWith :: forall m state a.
+     RunLockstep state m
+  => Bool -- ^ Verbose output
+  -> (Lockstep state, Lockstep state)
+  -> LockstepAction state a
+  -> LookUp m
+  -> Realized m a
+  -> PostconditionM m Bool
+postconditionWith verbose (before, _after) action _lookUp a =
     case checkResponse (Proxy @m) before action a of
-      Nothing -> pure True
-      Just s  -> monitorPost (QC.counterexample s) >> pure False
+      Right s
+        | verbose -> monitorPost (QC.counterexample s) >> pure True
+        | otherwise -> pure True
+      Left s  -> monitorPost (QC.counterexample s) >> pure False
 
 monitoring :: forall m state a.
      RunLockstep state m
@@ -155,7 +173,7 @@ instance InLockstep state => HasVariables (Action (Lockstep state) a) where
 checkResponse :: forall m state a.
      RunLockstep state m
   => Proxy m
-  -> Lockstep state -> LockstepAction state a -> Realized m a -> Maybe String
+  -> Lockstep state -> LockstepAction state a -> Realized m a -> Either String String
 checkResponse p (Lockstep state env) action a =
     compareEquality
       (a         , observeReal p action a)
@@ -166,23 +184,34 @@ checkResponse p (Lockstep state env) action a =
 
     compareEquality ::
          (Realized m a, Observable state a)
-      -> (ModelValue state a, Observable state a) -> Maybe String
+      -> (ModelValue state a, Observable state a) -> Either String String
     compareEquality (realResp, obsRealResp) (mockResp, obsMockResp)
-      | obsRealResp == obsMockResp = Nothing
-      | otherwise                  = Just $ concat [
+      | obsRealResp == obsMockResp = Right $ concat [
+            "System under test returned: "
+          , sutReturned
+          , "\nModel returned:             "
+          , modelReturned
+          ]
+      | otherwise                  = Left $ concat [
             "System under test returned: "
-          , case showRealResponse (Proxy @m) action of
-              Nothing   -> show obsRealResp
-              Just Dict -> concat [
-                  show obsRealResp
-                , " ("
-                , show realResp
-                , ")"
-                ]
+          , sutReturned
           , "\nbut model returned:         "
-          , show obsMockResp
-          , " ("
-          , show mockResp
-          , ")"
+          , modelReturned
           ]
 
+      where
+        sutReturned = case showRealResponse (Proxy @m) action of
+            Nothing   -> show obsRealResp
+            Just Dict -> concat [
+                show obsRealResp
+              , " ("
+              , show realResp
+              , ")"
+              ]
+
+        modelReturned = concat [
+              show obsMockResp
+            , " ("
+            , show mockResp
+            , ")"
+            ]

test/Main.hs

@@ -1,14 +1,16 @@
 module Main (main) where
 
-import Test.Tasty
+import           Test.Tasty
 
-import Test.IORef.Full   qualified
-import Test.IORef.Simple qualified
-import Test.MockFS       qualified
+import           Test.Golden
+import           Test.IORef.Full
+import           Test.IORef.Simple
+import           Test.MockFS
 
 main :: IO ()
 main = defaultMain $ testGroup "quickcheck-lockstep" [
-      Test.IORef.Simple.tests
+      Test.Golden.tests
+    , Test.IORef.Simple.tests
     , Test.IORef.Full.tests
     , Test.MockFS.tests
     ]

test/Test/Golden.hs

@@ -0,0 +1,107 @@
+{- HLINT ignore "Use camelCase" -}
+
+module Test.Golden where
+
+import           Control.Exception      (bracket_)
+import           System.Directory
+import           System.FilePath
+import           Test.MockFS            as MockFS
+import           Test.QuickCheck
+import           Test.QuickCheck.Random (mkQCGen)
+import           Test.Tasty
+import           Test.Tasty.Golden
+
+tests :: TestTree
+tests = testGroup "Test.Golden" [
+      golden_success_propLockstep_MockFS
+    , golden_failure_default_propLockstep_MockFS
+    , golden_failure_nonVerbose_propLockstep_MockFS
+    , golden_failure_verbose_propLockstep_MockFS
+    ]
+
+goldenDir :: FilePath
+goldenDir = "test" </> "golden"
+
+tmpDir :: FilePath
+tmpDir = "_tmp"
+
+-- | Golden test for a successful lockstep test
+golden_success_propLockstep_MockFS :: TestTree
+golden_success_propLockstep_MockFS =
+    goldenVsFile testName goldenPath outputPath $ do
+      createDirectoryIfMissing False tmpDir
+      r <- quickCheckWithResult args MockFS.propLockstep
+      writeFile outputPath (output r)
+  where
+    testName = "golden_success_propLockstep_MockFS"
+    goldenPath = goldenDir </> testName <.> "golden"
+    outputPath = tmpDir </> testName <.> "golden"
+
+    args = stdArgs {
+        replay = Just (mkQCGen 17, 32)
+      , chatty = False
+      }
+
+-- | Golden test for a failing lockstep test that produces a counterexample
+-- using the default postcondition.
+golden_failure_default_propLockstep_MockFS :: TestTree
+golden_failure_default_propLockstep_MockFS =
+    goldenVsFile testName goldenPath outputPath $ do
+      createDirectoryIfMissing False tmpDir
+      r <-
+        bracket_
+          MockFS.setInduceFault
+          MockFS.setNoInduceFault
+          (quickCheckWithResult args MockFS.propLockstep)
+      writeFile outputPath (output r)
+  where
+    testName = "golden_failure_default_propLockstep_MockFS"
+    goldenPath = goldenDir </> testName <.> "golden"
+    outputPath = tmpDir </> testName <.> "golden"
+
+    args = stdArgs {
+        replay = Just (mkQCGen 17, 32)
+      , chatty = False
+      }
+
+-- | Golden test for a failing lockstep test that produces a /non-verbose/ counterexample
+golden_failure_nonVerbose_propLockstep_MockFS :: TestTree
+golden_failure_nonVerbose_propLockstep_MockFS =
+    goldenVsFile testName goldenPath outputPath $ do
+      createDirectoryIfMissing False tmpDir
+      r <-
+        bracket_
+          (MockFS.setInduceFault >> MockFS.setPostconditionNonVerbose)
+          (MockFS.setNoInduceFault >> MockFS.setPostconditionDefault)
+          (quickCheckWithResult args MockFS.propLockstep)
+      writeFile outputPath (output r)
+  where
+    testName = "golden_failure_nonVerbose_propLockstep_MockFS"
+    goldenPath = goldenDir </> testName <.> "golden"
+    outputPath = tmpDir </> testName <.> "golden"
+
+    args = stdArgs {
+        replay = Just (mkQCGen 17, 32)
+      , chatty = False
+      }
+
+-- | Golden test for a failing lockstep test that produces a /verbose/ counterexample
+golden_failure_verbose_propLockstep_MockFS :: TestTree
+golden_failure_verbose_propLockstep_MockFS =
+    goldenVsFile testName goldenPath outputPath $ do
+      createDirectoryIfMissing False tmpDir
+      r <-
+        bracket_
+          (MockFS.setInduceFault >> MockFS.setPostconditionVerbose)
+          (MockFS.setNoInduceFault >> MockFS.setPostconditionDefault)
+          (quickCheckWithResult args MockFS.propLockstep)
+      writeFile outputPath (output r)
+  where
+    testName = "golden_failure_verbose_propLockstep_MockFS"
+    goldenPath = goldenDir </> testName <.> "golden"
+    outputPath = tmpDir </> testName <.> "golden"
+
+    args = stdArgs {
+        replay = Just (mkQCGen 17, 32)
+      , chatty = False
+      }