Initial stab at parallel actions (#94)

Author: MaximilianAlgehed

.github/workflows/haskell-ci.yml

@@ -40,7 +40,7 @@ jobs:
 
     strategy:
       matrix:
-        ghc-version: [latest, 9.12, "9.10", 9.8, 9.6, 9.4, 9.2, 9.0, "8.10"]
+        ghc-version: [latest, 9.12, "9.10", 9.8, 9.6, 9.4, 9.2, 9.0]
         os: [ubuntu-latest]
       fail-fast: false
 

cabal.project

@@ -4,3 +4,16 @@ packages:
 tests: true
 
 test-show-details: direct
+
+source-repository-package
+  type: git
+  location: https://github.com/input-output-hk/io-sim
+  subdir: io-sim
+  tag: 5683864d3c7300f9ee4a3430b4a590bb130cb88a
+
+
+source-repository-package
+  type: git
+  location: https://github.com/input-output-hk/io-sim
+  subdir: io-classes
+  tag: 5683864d3c7300f9ee4a3430b4a590bb130cb88a

quickcheck-dynamic/CHANGELOG.md

@@ -7,6 +7,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 As a minor extension, we also keep a semantic version for the `UNRELEASED`
 changes.
 
+## UNRELEASED
+
+* **BREAKING**: Removed `m` parameter from `PostConditionM` as this is not generally safe.
+* **BREAKING**: Additional `Show` constraint on the result of actions
+* A new module `Test.QuickCheck.ParallelActions` that implements testing linearizability of a model
+  when running in parallel.
+* Additional `Property` combinators `sometimes` and `always`
+
 ## 4.0.0 - 2025-03-12
 
 * **BREAKING**: Removed `Realized`

quickcheck-dynamic/quickcheck-dynamic.cabal

@@ -6,6 +6,7 @@ license-files:
   LICENSE
   NOTICE
 
+Tested-with: GHC >= 9.0 && < 9.13
 maintainer:         [email protected]
 author:             Ulf Norell
 category:           Testing
@@ -27,6 +28,9 @@ source-repository head
   type:     git
   location: https://github.com/input-output-hk/quickcheck-dynamic
 
+flag dev
+  default: False
+
 common lang
   default-language:   Haskell2010
   default-extensions:
@@ -62,6 +66,7 @@ common lang
     -Wall -Wnoncanonical-monad-instances -Wunused-packages
     -Wincomplete-uni-patterns -Wincomplete-record-updates
     -Wredundant-constraints -Widentities -Wno-unused-do-bind
+    -Wno-name-shadowing -Wno-x-partial
 
 library
   import:          lang
@@ -76,6 +81,23 @@ library
     Test.QuickCheck.Extras
     Test.QuickCheck.StateModel
     Test.QuickCheck.StateModel.Variables
+    Test.QuickCheck.ParallelActions
+
+  if flag(dev)
+    hs-source-dirs: test
+    exposed-modules:
+      Spec.DynamicLogic.Counters
+      Spec.DynamicLogic.Registry
+      Spec.DynamicLogic.RegistryModel
+      Test.QuickCheck.DynamicLogic.QuantifySpec
+      Test.QuickCheck.StateModelSpec
+    build-depends:
+      , io-classes
+      , io-sim
+      , stm
+      , tasty
+      , tasty-hunit
+      , tasty-quickcheck
 
   build-depends:
     , base        >=4.7 && <5
@@ -100,6 +122,8 @@ test-suite quickcheck-dynamic-test
   build-depends:
     , base
     , containers
+    , io-classes
+    , io-sim
     , mtl
     , QuickCheck
     , quickcheck-dynamic

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

@@ -60,10 +60,10 @@ instance Monad (DL s) where
 instance MonadFail (DL s) where
   fail = errorDL
 
-action :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)
+action :: (Typeable a, Show a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)
 action cmd = DL $ \_ k -> DL.after cmd k
 
-failingAction :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s ()
+failingAction :: (Typeable a, Show a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s ()
 failingAction cmd = DL $ \_ k -> DL.afterNegative cmd (k ())
 
 anyAction :: DL s ()
@@ -96,7 +96,7 @@ getModelStateDL = DL $ \s k -> k (underlyingState s) s
 getVarContextDL :: DL s VarContext
 getVarContextDL = DL $ \s k -> k (vars s) s
 
-forAllVar :: forall a s. Typeable a => DL s (Var a)
+forAllVar :: forall a s. (Typeable a, Show a) => DL s (Var a)
 forAllVar = do
   xs <- ctxAtType <$> getVarContextDL
   forAllQ $ elementsQ xs

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

@@ -33,7 +33,7 @@ data DynLogic s
     Stopping (DynLogic s)
   | -- | After a specific action the predicate should hold
     forall a.
-    (Eq (Action s a), Show (Action s a), Typeable a) =>
+    (Eq (Action s a), Show (Action s a), Typeable a, Show a) =>
     After (ActionWithPolarity s a) (Var a -> DynPred s)
   | Error String (DynPred s)
   | -- | Adjust the probability of picking a branch
@@ -66,7 +66,7 @@ afterAny :: (Annotated s -> DynFormula s) -> DynFormula s
 afterAny f = DynFormula $ \n -> AfterAny $ \s -> unDynFormula (f s) n
 
 afterPolar
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => ActionWithPolarity s a
   -> (Var a -> Annotated s -> DynFormula s)
   -> DynFormula s
@@ -75,7 +75,7 @@ afterPolar act f = DynFormula $ \n -> After act $ \x s -> unDynFormula (f x s) n
 -- | Given `f` must be `True` after /some/ action.
 -- `f` is passed the state resulting from executing the `Action`.
 after
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => Action s a
   -> (Var a -> Annotated s -> DynFormula s)
   -> DynFormula s
@@ -85,7 +85,7 @@ after act f = afterPolar (ActionWithPolarity act PosPolarity) f
 -- `f` is passed the state resulting from executing the `Action`
 -- as a negative action.
 afterNegative
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => Action s a
   -> (Annotated s -> DynFormula s)
   -> DynFormula s

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

@@ -2,6 +2,7 @@ module Test.QuickCheck.Extras where
 
 import Control.Monad.Reader
 import Control.Monad.State
+import Test.QuickCheck
 import Test.QuickCheck.Monadic
 
 runPropertyStateT :: Monad m => PropertyM (StateT s m) a -> s -> PropertyM m (a, s)
@@ -13,3 +14,9 @@ runPropertyReaderT :: Monad m => PropertyM (ReaderT e m) a -> e -> PropertyM m a
 runPropertyReaderT p e = MkPropertyM $ \k -> do
   m <- unPropertyM p $ fmap lift . k
   return $ runReaderT m e
+
+sometimes :: Testable p => Int -> p -> Property
+sometimes i = disjoin . replicate i
+
+always :: Testable p => Int -> p -> Property
+always i = conjoin . replicate i