Generalize postcondition

quickcheck-dynamic/quickcheck-dynamic.cabal

@@ -5,12 +5,12 @@ license:         Apache-2.0
 license-files:
   LICENSE
   NOTICE
-  
+
 maintainer:      [email protected]
 author:          Ulf Norell
 category:        Testing
 synopsis:
-  A library for stateful property-based testing   
+  A library for stateful property-based testing
 homepage:
   https://github.com/input-output-hk/quickcheck-dynamic#readme
 
@@ -23,7 +23,7 @@ description:
 build-type:      Simple
 extra-doc-files: README.md
 extra-source-files: CHANGELOG.md
-                    
+
 source-repository head
   type:     git
   location: https://github.com/input-output-hk/quickcheck-dynamic
@@ -58,6 +58,7 @@ library
         Test.QuickCheck.DynamicLogic.SmartShrinking
         Test.QuickCheck.DynamicLogic.Utils
         Test.QuickCheck.StateModel
+        Test.QuickCheck.StateModel.Postcondition
     build-depends:
         QuickCheck -any,
         base >=4.7 && <5,

quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs

@@ -39,10 +39,13 @@ module Test.QuickCheck.StateModel (
 
 import Control.Monad
 import Data.Data
-import Test.QuickCheck as QC
+import Test.QuickCheck as QC hiding ((===))
 import Test.QuickCheck.DynamicLogic.SmartShrinking
 import Test.QuickCheck.Monadic
 
+import Test.QuickCheck.StateModel.Postcondition (Postcondition(..))
+import Test.QuickCheck.StateModel.Postcondition qualified as Post
+
 -- | The typeclass users implement to define a model against which to validate some implementation.
 --
 -- To implement a `StateModel`, user needs to provide at least the following:
@@ -114,7 +117,7 @@ class
   -- by `perform`ing the `Action` inside the `state` so that further actions can use `Lookup`
   -- to retrieve that data. This allows the model to be ignorant of those values yet maintain
   -- some references that can be compared and looked for.
-  nextState :: state -> Action state a -> Var a -> state
+  nextState :: Typeable a => state -> Action state a -> Var a -> state
   nextState s _ _ = s
 
   -- | Precondition for filtering generated `Action`.
@@ -124,10 +127,11 @@ class
   precondition _ _ = True
 
   -- | Postcondition on the `a` value produced at some step.
-  -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
-  -- to check the implementation produces expected values.
-  postcondition :: state -> Action state a -> LookUp -> a -> Bool
-  postcondition _ _ _ _ = True
+  --
+  -- When 'postcondition' returns @Just err@, the property will fail, and @err@ will be shown as a
+  -- counter-example. This is useful to check th implementation produces expected values.
+  postcondition :: state -> Action state a -> LookUp -> a -> Postcondition
+  postcondition _ _ _ _ = Post.assertSuccess
 
   -- | Allows the user to attach information to the `Property` at each step of the process.
   -- This function is given the full transition that's been executed, including the start and ending
@@ -338,5 +342,10 @@ runActionsInState state RunModel{..} (Actions_ rejected (Smart _ actions)) = loo
     let s' = nextState s act (Var n)
         env' = (Var n :== ret) : env
     monitor (monitoring (s, s') act (lookUpVar env') ret)
-    assert $ postcondition s act (lookUpVar env) ret
+    case getPostcondition $ postcondition s act (lookUpVar env) ret of
+      Right () -> return ()
+      Left err -> do
+        monitor (counterexample err)
+        assert False
     loop s' env' as
+

quickcheck-dynamic/src/Test/QuickCheck/StateModel/Postcondition.hs

@@ -0,0 +1,100 @@
+-- | Result of evaluation the postcondition
+--
+-- See 'Test.QuickCheck.StateModel.postcondition'.
+--
+-- Intended for qualified import.
+--
+-- > import Test.QuickCheck.StateModel.Postcondition (Postcondition(..))
+-- > import Test.QuickCheck.StateModel.Postcondition qualified as Post
+module Test.QuickCheck.StateModel.Postcondition (
+    Postcondition(..)
+    -- * Primitives
+  , assertSuccess
+  , assertFailure
+  , assertRelatedBy
+  , assertBool
+  , assertEQ
+  , assertLE
+  , assertLT
+  , assertLeft
+  , assertRight
+    -- * Combinators
+  , and
+  , all
+  , map
+  ) where
+
+import Prelude hiding (and, all, map)
+import Prelude qualified
+
+import Data.Bifunctor (bimap)
+import Data.Foldable (toList)
+import GHC.Show (appPrec1, showSpace)
+
+-- | Result of 'postcondition'
+newtype Postcondition = Postcondition { getPostcondition :: Either String () }
+  deriving (Show)
+
+{-------------------------------------------------------------------------------
+  Primitives
+-------------------------------------------------------------------------------}
+
+assertSuccess :: Postcondition
+assertSuccess = Postcondition $ Right ()
+
+assertFailure :: String -> Postcondition
+assertFailure = Postcondition . Left
+
+assertBool :: String -> Bool -> Postcondition
+assertBool _   True  = Postcondition $ Right ()
+assertBool msg False = assertFailure msg
+
+-- | Assert that two values are related by the given relation
+--
+-- The first argument should be a string representation representing the
+-- negated relation. For example:
+--
+-- > assertEqual = assertRelatedBy "/=" (==)
+assertRelatedBy :: Show a => String -> (a -> a -> Bool) -> a -> a -> Postcondition
+assertRelatedBy op f x y = Postcondition $
+    if f x y
+      then Right ()
+      else Left $ showsPrec appPrec1 x
+                . showSpace
+                . showString op
+                . showSpace
+                . showsPrec appPrec1 y
+                $ ""
+
+assertEQ :: (Eq a, Show a) => a -> a -> Postcondition
+assertEQ = assertRelatedBy "/=" (==)
+
+assertLT :: (Ord a, Show a) => a -> a -> Postcondition
+assertLT = assertRelatedBy ">=" (<)
+
+assertLE :: (Ord a, Show a) => a -> a -> Postcondition
+assertLE = assertRelatedBy ">" (<=)
+
+assertLeft :: Show b => Either a b -> Postcondition
+assertLeft (Left  _)  = assertSuccess
+assertLeft (Right b) = assertFailure $ "Expected Left: " ++ show b
+
+assertRight :: Show a => Either a b -> Postcondition
+assertRight (Right _) = assertSuccess
+assertRight (Left  a) = assertFailure $ "Expected Right: " ++ show a
+
+{-------------------------------------------------------------------------------
+  Combinators
+-------------------------------------------------------------------------------}
+
+map :: (String -> String) -> Postcondition -> Postcondition
+map f = Postcondition . bimap f id . getPostcondition
+
+and :: Foldable t => t Postcondition -> Postcondition
+and = Postcondition . sequence_ . Prelude.map getPostcondition . toList
+
+all :: forall t a. (Foldable t, Show a) => (a -> Postcondition) -> t a -> Postcondition
+all f = and . Prelude.map aux . toList
+  where
+    aux :: a -> Postcondition
+    aux a = map (\msg -> show a ++ ": " ++ msg) (f a)

quickcheck-io-sim-compat/test/Spec/DynamicLogic/RegistryModel.hs

@@ -34,6 +34,7 @@ import Spec.DynamicLogic.Registry
 import Test.QuickCheck.DynamicLogic.Core
 import Test.QuickCheck.StateModel
 import Test.QuickCheck.StateModel.IOSim
+import Test.QuickCheck.StateModel.Postcondition qualified as Post
 
 data RegState = RegState
   { tids :: [Var ModelThreadId]
@@ -126,15 +127,15 @@ instance StateModel RegState where
   precondition s (Successful act) = precondition s act
   precondition _ _ = True
 
-  postcondition _ Init _ _ = True
-  postcondition s (WhereIs name) env mtid =
-    (env <$> lookup name (regs s)) == mtid
-  postcondition _s Spawn _ _ = True
-  postcondition s (Register name step) _ res =
-    positive s (Register name step) == isRight res
-  postcondition _s (Unregister _name) _ _ = True
-  postcondition _s (KillThread _) _ _ = True
-  postcondition _s (Successful (Register _ _)) _ res = isRight res
+  postcondition _ Init _ _ = Post.assertSuccess
+  postcondition s (WhereIs name) env mtid = Post.assertEQ mtid $
+    (env <$> lookup name (regs s))
+  postcondition _s Spawn _ _ = Post.assertSuccess
+  postcondition s (Register name step) _ res = Post.assertEQ (isRight res) $
+    positive s (Register name step)
+  postcondition _s (Unregister _name) _ _ = Post.assertSuccess
+  postcondition _s (KillThread _) _ _ = Post.assertSuccess
+  postcondition _s (Successful (Register _ _)) _ res = Post.assertRight res
   postcondition s (Successful act) env res = postcondition s act env res
 
   monitoring (_s, s') act _ res =