Refactor runActions to distinguish more clearly various cases (#71)

* Refactor runActions to distinguish more clearly various cases

As I was looking for ways to implement parallel testing in q-d, I tried to understand what was going on with actions execution and I have attempted to expose more explicitly the various execution branches. This lead some simplification in the ways post-condition are computed.

* Use full words instead of abbreviations in smart shrinker definition
* Simplify runActions
* Consolidate various counter models in a single module

Author: Arnaud Bailly

quickcheck-dynamic/quickcheck-dynamic.cabal

@@ -90,10 +90,11 @@ test-suite quickcheck-dynamic-test
   main-is:        Spec.hs
   hs-source-dirs: test
   other-modules:
-    Spec.DynamicLogic.CounterModel
+    Spec.DynamicLogic.Counters
     Spec.DynamicLogic.Registry
     Spec.DynamicLogic.RegistryModel
     Test.QuickCheck.DynamicLogic.QuantifySpec
+    Test.QuickCheck.StateModelSpec
 
   ghc-options:    -rtsopts
   build-depends:
@@ -104,4 +105,5 @@ test-suite quickcheck-dynamic-test
     , quickcheck-dynamic
     , stm
     , tasty
+    , tasty-hunit
     , tasty-quickcheck

quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs

@@ -3,12 +3,16 @@ module Test.QuickCheck.DynamicLogic.SmartShrinking (shrinkSmart) where
 import Test.QuickCheck
 
 -- | This combinator captures the 'smart shrinking' implemented for the
--- Smart type wrapper in Test.QuickCheck.Modifiers.
+-- `Smart` type wrapper in [Test.QuickCheck.Modifiers](https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Modifiers.html#t:Smart).
+-- It interleaves the output of the given shrinker to try to converge to more
+-- interesting values faster.
 shrinkSmart :: (a -> [a]) -> Smart a -> [Smart a]
-shrinkSmart shr (Smart i x) = take i' ys `ilv` drop i' ys
+shrinkSmart shrinker (Smart i x) = take i' ys `interleave` drop i' ys
   where
-    ys = [Smart j y | (j, y) <- [0 ..] `zip` shr x]
+    ys = [Smart j y | (j, y) <- [0 ..] `zip` shrinker x]
+
     i' = 0 `max` (i - 2)
-    [] `ilv` bs = bs
-    as `ilv` [] = as
-    (a : as) `ilv` (b : bs) = a : b : (as `ilv` bs)
+
+    [] `interleave` bs = bs
+    as `interleave` [] = as
+    (a : as) `interleave` (b : bs) = a : b : (as `interleave` bs)

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

@@ -2,7 +2,7 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 
--- | Simple (stateful) Model-Based Testing library for use with Haskell QuickCheck.
+-- | Model-Based Testing library for use with Haskell QuickCheck.
 --
 -- This module provides the basic machinery to define a `StateModel` from which /traces/ can
 -- be generated and executed against some /actual/ implementation code to define monadic `Property`
@@ -32,6 +32,7 @@ module Test.QuickCheck.StateModel (
   runActions,
   lookUpVar,
   lookUpVarMaybe,
+  viewAtType,
   initialAnnotatedState,
   computeNextState,
   computePrecondition,
@@ -192,6 +193,13 @@ newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property,
 instance MonadTrans PostconditionM where
   lift = PostconditionM . lift
 
+evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m ()
+evaluatePostCondition post = do
+  (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ post
+  monitor mon
+  unless b $ monitor onFail
+  assert b
+
 -- | Apply the property transformation to the property after evaluating
 -- the postcondition. Useful for collecting statistics while avoiding
 -- duplication between `monitoring` and `postcondition`.
@@ -239,23 +247,6 @@ class (forall a. Show (Action state a), Monad m) => RunModel state m where
   monitoringFailure :: state -> Action state a -> LookUp m -> Error state -> Property -> Property
   monitoringFailure _ _ _ _ prop = prop
 
-computePostcondition
-  :: forall m state a
-   . RunModel state m
-  => (state, state)
-  -> ActionWithPolarity state a
-  -> LookUp m
-  -> Either (Error state) (Realized m a)
-  -> PostconditionM m Bool
-computePostcondition ss (ActionWithPolarity a p) l r
-  | p == PosPolarity = case r of
-      Right ra -> postcondition ss a l ra
-      -- NOTE: this is actually redundant as this handled
-      -- at the call site for this function, but this is
-      -- good hygiene?
-      Left _ -> pure False
-  | otherwise = postconditionOnFailure ss a l r
-
 type LookUp m = forall a. Typeable a => Var a -> Realized m a
 
 type Env m = [EnvEntry m]
@@ -515,47 +506,82 @@ runActions
      )
   => Actions state
   -> PropertyM m (Annotated state, Env m)
-runActions (Actions_ rejected (Smart _ actions)) = loop initialAnnotatedState [] actions
+runActions (Actions_ rejected (Smart _ actions)) = do
+  (finalState, env) <- runSteps initialAnnotatedState [] actions
+  unless (null rejected) $
+    monitor $
+      tabulate "Actions rejected by precondition" rejected
+  return (finalState, env)
+
+-- | Core function to execute a sequence of `Step` given some initial `Env`ironment
+-- and `Annotated` state.
+runSteps
+  :: forall state m e
+   . ( StateModel state
+     , RunModel state m
+     , e ~ Error state
+     , forall a. IsPerformResult e a
+     )
+  => Annotated state
+  -> Env m
+  -> [Step state]
+  -> PropertyM m (Annotated state, Env m)
+runSteps s env [] = return (s, reverse env)
+runSteps s env ((v := act) : as) = do
+  pre $ computePrecondition s act
+  ret <- run $ performResultToEither <$> perform (underlyingState s) action (lookUpVar env)
+  let name = show polar ++ actionName action
+  monitor $ tabulate "Actions" [name]
+  monitor $ tabulate "Action polarity" [show polar]
+  case (polar, ret) of
+    (PosPolarity, Left err) ->
+      positiveActionFailed err
+    (PosPolarity, Right val) -> do
+      (s', env') <- positiveActionSucceeded ret val
+      runSteps s' env' as
+    (NegPolarity, _) -> do
+      (s', env') <- negativeActionResult ret
+      runSteps s' env' as
   where
-    loop :: Annotated state -> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
-    loop _s env [] = do
-      unless (null rejected) $
-        monitor $
-          tabulate "Actions rejected by precondition" rejected
-      return (_s, reverse env)
-    loop s env ((v := act) : as) = do
-      pre $ computePrecondition s act
-      ret <- run $ performResultToEither <$> perform (underlyingState s) (polarAction act) (lookUpVar env)
-      let name = show (polarity act) ++ actionName (polarAction act)
-      monitor $ tabulate "Actions" [name]
-      monitor $ tabulate "Action polarity" [show $ polarity act]
-      if
-        | polarity act == PosPolarity
-        , Left err <- ret -> do
-            monitor $
-              monitoringFailure @state @m
-                (underlyingState s)
-                (polarAction act)
-                (lookUpVar env)
-                err
-            stop False
-        | otherwise -> do
-            let var = unsafeCoerceVar v
-                s' = computeNextState s act var
-                env'
-                  | Right val <- ret = (var :== val) : env
-                  | otherwise = env
-            monitor $ monitoring @state @m (underlyingState s, underlyingState s') (polarAction act) (lookUpVar env') ret
-            (b, (Endo mon, Endo onFail)) <-
-              run
-                . runWriterT
-                . runPost
-                $ computePostcondition @m
-                  (underlyingState s, underlyingState s')
-                  act
-                  (lookUpVar env)
-                  ret
-            monitor mon
-            unless b $ monitor onFail
-            assert b
-            loop s' env' as
+    polar = polarity act
+
+    action = polarAction act
+
+    positiveActionFailed err = do
+      monitor $
+        monitoringFailure @state @m
+          (underlyingState s)
+          action
+          (lookUpVar env)
+          err
+      stop False
+
+    positiveActionSucceeded ret val = do
+      (s', env', stateTransition) <- computeNewState ret
+      evaluatePostCondition $
+        postcondition
+          stateTransition
+          action
+          (lookUpVar env)
+          val
+      pure (s', env')
+
+    negativeActionResult ret = do
+      (s', env', stateTransition) <- computeNewState ret
+      evaluatePostCondition $
+        postconditionOnFailure
+          stateTransition
+          action
+          (lookUpVar env)
+          ret
+      pure (s', env')
+
+    computeNewState ret = do
+      let var = unsafeCoerceVar v
+          s' = computeNextState s act var
+          env'
+            | Right val <- ret = (var :== val) : env
+            | otherwise = env
+          stateTransition = (underlyingState s, underlyingState s')
+      monitor $ monitoring @state @m stateTransition action (lookUpVar env') ret
+      pure (s', env', stateTransition)

quickcheck-dynamic/test/Spec.hs

@@ -2,9 +2,9 @@
 
 module Main (main) where
 
-import Spec.DynamicLogic.CounterModel qualified
 import Spec.DynamicLogic.RegistryModel qualified
 import Test.QuickCheck.DynamicLogic.QuantifySpec qualified
+import Test.QuickCheck.StateModelSpec qualified
 import Test.Tasty
 
 main :: IO ()
@@ -15,6 +15,6 @@ tests =
   testGroup
     "dynamic logic"
     [ Spec.DynamicLogic.RegistryModel.tests
-    , Spec.DynamicLogic.CounterModel.tests
     , Test.QuickCheck.DynamicLogic.QuantifySpec.tests
+    , Test.QuickCheck.StateModelSpec.tests
     ]

quickcheck-dynamic/test/Spec/DynamicLogic/CounterModel.hs

@@ -0,0 +1,97 @@
+{-# LANGUAGE NamedFieldPuns #-}
+
+-- | Define several variant models of /counters/ which are useful to
+-- test or use examples for various behaviours of the runtime.
+module Spec.DynamicLogic.Counters where
+
+import Control.Monad.Reader
+import Data.IORef
+import Test.QuickCheck
+import Test.QuickCheck.StateModel
+
+-- A very simple model with a single action that always succeed in
+-- predictable way. This model is useful for testing the runtime.
+newtype SimpleCounter = SimpleCounter {count :: Int}
+  deriving (Eq, Show, Generic)
+
+deriving instance Eq (Action SimpleCounter a)
+deriving instance Show (Action SimpleCounter a)
+instance HasVariables (Action SimpleCounter a) where
+  getAllVariables _ = mempty
+
+instance StateModel SimpleCounter where
+  data Action SimpleCounter a where
+    IncSimple :: Action SimpleCounter Int
+
+  arbitraryAction _ _ = pure $ Some IncSimple
+
+  initialState = SimpleCounter 0
+
+  nextState SimpleCounter{count} IncSimple _ = SimpleCounter (count + 1)
+
+instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where
+  perform _ IncSimple _ = do
+    ref <- ask
+    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+
+-- A very simple model with a single action whose postcondition fails in a
+-- predictable way. This model is useful for testing the runtime.
+newtype FailingCounter = FailingCounter {failingCount :: Int}
+  deriving (Eq, Show, Generic)
+
+deriving instance Eq (Action FailingCounter a)
+deriving instance Show (Action FailingCounter a)
+instance HasVariables (Action FailingCounter a) where
+  getAllVariables _ = mempty
+
+instance StateModel FailingCounter where
+  data Action FailingCounter a where
+    Inc' :: Action FailingCounter Int
+
+  arbitraryAction _ _ = pure $ Some Inc'
+
+  initialState = FailingCounter 0
+
+  nextState FailingCounter{failingCount} Inc' _ = FailingCounter (failingCount + 1)
+
+instance RunModel FailingCounter (ReaderT (IORef Int) IO) where
+  perform _ Inc' _ = do
+    ref <- ask
+    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+
+  postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4
+
+-- A generic but simple counter model
+data Counter = Counter Int
+  deriving (Show, Generic)
+
+deriving instance Show (Action Counter a)
+deriving instance Eq (Action Counter a)
+instance HasVariables (Action Counter a) where
+  getAllVariables _ = mempty
+
+instance StateModel Counter where
+  data Action Counter a where
+    Inc :: Action Counter ()
+    Reset :: Action Counter Int
+
+  initialState = Counter 0
+
+  arbitraryAction _ _ = frequency [(5, pure $ Some Inc), (1, pure $ Some Reset)]
+
+  nextState (Counter n) Inc _ = Counter (n + 1)
+  nextState _ Reset _ = Counter 0
+
+instance RunModel Counter (ReaderT (IORef Int) IO) where
+  perform _ Inc _ = do
+    ref <- ask
+    lift $ modifyIORef ref succ
+  perform _ Reset _ = do
+    ref <- ask
+    lift $ do
+      n <- readIORef ref
+      writeIORef ref 0
+      pure n
+
+  postcondition (Counter n, _) Reset _ res = pure $ n == res
+  postcondition _ _ _ _ = pure True