Improvements to IOSim compatibility

.github/workflows/ci.yaml

@@ -26,7 +26,7 @@ jobs:
       with:
         extra_nix_config: |
           trusted-public-keys = iohk.cachix.org-1:DpRUyj7h7V830dp/i6Nti+NEO2/nhblbov/8MW7Rqoo= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
-          substituters = https://cache.nixos.org https://cache.iog.io https://iohk.cachix.org
+          substituters = https://cache.nixos.org https://hydra.iohk.io https://iohk.cachix.org
 
     - name: Github cache ~/.cabal/packages, ~/.cabal/store and dist-newstyle
       uses: actions/[email protected]

cabal.project

@@ -1,6 +1,6 @@
 packages:
   quickcheck-dynamic
-  quickcheck-io-sim-compat
+  quickcheck-dynamic-iosim
 
 tests: true
 

fmt.sh

@@ -0,0 +1,2 @@
+#!/bin/bash
+find . -type f -name *.hs | xargs -n1 fourmolu -i

quickcheck-io-sim-compat/quickcheck-io-sim-compat.cabal → quickcheck-dynamic-iosim/quickcheck-dynamic-iosim.cabal

@@ -1,11 +1,11 @@
 cabal-version:   2.2
-name:            quickcheck-io-sim-compat
+name:            quickcheck-dynamic-iosim
 version:         0.1.0.0
 license:         Apache-2.0
 license-files:
   LICENSE
   NOTICE
-  CHANGELOG.md
+
 category:  Testing
 synopsis:
   A library to implement stateful property-based testing using dynamic logic.
@@ -53,15 +53,13 @@ library
     exposed-modules:
         Test.QuickCheck.StateModel.IOSim
     build-depends:
-        QuickCheck -any,
         base >=4.7 && <5,
         io-classes,
         io-sim,
-        lens,
-        containers,
-        mtl
+        stm,
+        quickcheck-dynamic
 
-test-suite quickcheck-io-sim-compat-test
+test-suite quickcheck-dynamic-iosim
     import: lang
     type: exitcode-stdio-1.0
     main-is: Spec.hs
@@ -74,7 +72,7 @@ test-suite quickcheck-io-sim-compat-test
         QuickCheck -any,
         base >=4.7 && <5,
         quickcheck-dynamic -any,
-        quickcheck-io-sim-compat -any,
+        quickcheck-dynamic-iosim -any,
         tasty -any,
         tasty-test-reporter -any,
         tasty-quickcheck -any,

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

@@ -0,0 +1,41 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-name-shadowing #-}
+
+module Test.QuickCheck.StateModel.IOSim where
+
+import Control.Concurrent
+import Control.Concurrent.STM
+import Control.Monad.Class.MonadFork qualified as IOClass
+import Control.Monad.Class.MonadSTM qualified as IOClass
+import Control.Monad.IOSim
+
+-- TODO: when we've updated the dependency on io-sim
+-- import Control.Monad.Class.MonadMVar qualified as IOClass
+
+import Test.QuickCheck.StateModel
+
+type family RealizeIOSim s a where
+  RealizeIOSim s ThreadId = IOClass.ThreadId (IOSim s)
+  RealizeIOSim s (TVar a) = IOClass.TVar (IOSim s) a
+-- TODO: when we've updated the dependency on io-sim
+-- RealizeIOSim s (MVar a) = IOClass.MVar (IOSim s) a
+-- TODO: unfortunately no poly-kinded recursion for type families
+-- so we can't do something like :'(
+-- RealizeIOSim s (f a)    = (RealizeIOSim f) (RealizeIOSim s a)
+  RealizeIOSim s (f a b) = f (RealizeIOSim s a) (RealizeIOSim s b)
+  RealizeIOSim s (f a) = f (RealizeIOSim s a)
+  RealizeIOSim s a = a
+
+type instance Realized (IOSim s) a = RealizeIOSim s a

quickcheck-io-sim-compat/test/Spec.hs → quickcheck-dynamic-iosim/test/Spec.hs

@@ -4,7 +4,7 @@ module Main (main) where
 
 import Spec.DynamicLogic.RegistryModel qualified
 import Test.Tasty
-import qualified Test.Tasty.Runners.Reporter as Reporter
+import Test.Tasty.Runners.Reporter qualified as Reporter
 
 main :: IO ()
 main = defaultMainWithIngredients [Reporter.ingredient] tests

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

@@ -8,14 +8,16 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Spec.DynamicLogic.RegistryModel where
 
---import Control.Concurrent
+import Control.Concurrent (ThreadId)
 import Control.Exception (SomeException (..))
-import Control.Monad.Class.MonadFork
+import Control.Monad.Class.MonadFork hiding (ThreadId)
+import Control.Monad.Class.MonadFork qualified as IOClass
 
 import Control.Monad.Class.MonadThrow (try)
 import Control.Monad.Class.MonadTimer (threadDelay)
@@ -33,12 +35,12 @@ import Test.Tasty.QuickCheck (testProperty)
 import Spec.DynamicLogic.Registry
 import Test.QuickCheck.DynamicLogic.Core
 import Test.QuickCheck.StateModel
-import Test.QuickCheck.StateModel.IOSim
+import Test.QuickCheck.StateModel.IOSim ()
 
 data RegState = RegState
-  { tids :: [Var ModelThreadId]
-  , regs :: [(String, Var ModelThreadId)]
-  , dead :: [Var ModelThreadId]
+  { tids :: [Var ThreadId]
+  , regs :: [(String, Var ThreadId)]
+  , dead :: [Var ThreadId]
   , setup :: Bool
   }
   deriving (Show)
@@ -49,11 +51,11 @@ deriving instance Eq (Action RegState a)
 instance StateModel RegState where
   data Action RegState a where
     Init :: Action RegState ()
-    Spawn :: Action RegState ModelThreadId
-    WhereIs :: String -> Action RegState (Maybe ModelThreadId)
-    Register :: String -> Var ModelThreadId -> Action RegState (Either SomeException ())
+    Spawn :: Action RegState ThreadId
+    WhereIs :: String -> Action RegState (Maybe ThreadId)
+    Register :: String -> Var ThreadId -> Action RegState (Either SomeException ())
     Unregister :: String -> Action RegState (Either SomeException ())
-    KillThread :: Var ModelThreadId -> Action RegState ()
+    KillThread :: Var ThreadId -> Action RegState ()
     -- not generated
     Successful :: Action RegState a -> Action RegState a
 
@@ -108,7 +110,7 @@ instance StateModel RegState where
     s{tids = step : tids s}
   nextState s (Register name tid) _step
     | positive s (Register name tid) =
-      s{regs = (name, tid) : regs s}
+        s{regs = (name, tid) : regs s}
     | otherwise = s
   nextState s (Unregister name) _step =
     s{regs = filter ((/= name) . fst) (regs s)}
@@ -126,15 +128,37 @@ 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
+type RegM s = StateT (Registry (IOSim s)) (IOSim s)
+
+instance (m ~ RegM s) => RunModel RegState m where
+  perform _ Init _ = do
+    reg <- lift setupRegistry
+    put reg
+  perform _ Spawn _ = do
+    lift $ forkIO (threadDelay 10000000)
+  perform _ (Register name tid) env = do
+    reg <- get
+    lift $ try $ register reg name (env tid)
+  perform _ (Unregister name) _ = do
+    reg <- get
+    lift $ try $ unregister reg name
+  perform _ (WhereIs name) _ = do
+    reg <- get
+    lift $ whereis reg name
+  perform _ (KillThread tid) env = do
+    lift $ killThread (env tid)
+  perform s (Successful act) env = do
+    perform s act env
+
+  postcondition _ Init _ _ = pure True
+  postcondition (s, _) (WhereIs name) env mtid =
+    pure $ (env <$> lookup name (regs s)) == mtid
+  postcondition _s Spawn _ _ = pure True
+  postcondition (s, _) (Register name step) _ res =
+    pure $ positive s (Register name step) == isRight res
+  postcondition _s (Unregister _name) _ _ = pure True
+  postcondition _s (KillThread _) _ _ = pure True
+  postcondition _s (Successful (Register _ _)) _ res = pure $ isRight res
   postcondition s (Successful act) env res = postcondition s act env res
 
   monitoring (_s, s') act _ res =
@@ -152,35 +176,6 @@ instance StateModel RegState where
         WhereIs _ -> tabu "WhereIs" [case res of Nothing -> "fails"; Just _ -> "succeeds"]
         _ -> id
 
-runModelIOSim :: forall s. RunModel RegState (IOSimModel (Registry (IOSim s)) s)
-runModelIOSim = RunModel performRegistry
- where
-  performRegistry :: forall a. RegState -> Action RegState a -> LookUp -> IOSimModel (Registry (IOSim s)) s a
-  performRegistry _ Init _ = do
-    reg <- liftIOSim setupRegistry
-    put reg
-  performRegistry _ Spawn _ =
-    encapsulateM $ forkIO (threadDelay 10000000)
-  performRegistry _ (Register name tid) env =
-    do
-      reg <- get
-      tid' <- instantiateM (env tid)
-      liftIOSim $ try $ register reg name tid'
-  performRegistry _ (Unregister name) _ =
-    do
-      reg <- get
-      liftIOSim $ try $ unregister reg name
-  performRegistry _ (WhereIs name) _ =
-    do
-      reg <- get
-      encapsulateM $ whereis reg name
-  performRegistry _ (KillThread tid) env =
-    do
-      tid' <- instantiateM (env tid)
-      liftIOSim $ killThread tid'
-  performRegistry s (Successful act) env =
-    performRegistry s act env
-
 positive :: RegState -> Action RegState a -> Bool
 positive s (Register name tid) =
   name `notElem` map fst (regs s)
@@ -198,7 +193,7 @@ why :: RegState -> Action RegState a -> String
 why s (Register name tid) =
   unwords $
     ["name already registered" | name `elem` map fst (regs s)]
-    ++ ["tid already registered" | tid `elem` map snd (regs s)]
+      ++ ["tid already registered" | tid `elem` map snd (regs s)]
       ++ ["dead thread" | tid `elem` dead s]
 why _ _ = "(impossible)"
 
@@ -217,7 +212,7 @@ shrinkName name = [n | n <- allNames, n < name]
 allNames :: [String]
 allNames = ["a", "b", "c", "d", "e"]
 
-shrinkTid :: RegState -> Var ModelThreadId -> [Var ModelThreadId]
+shrinkTid :: RegState -> Var ThreadId -> [Var ThreadId]
 shrinkTid s tid = [tid' | tid' <- tids s, tid' < tid]
 
 tabu :: String -> [String] -> Property -> Property
@@ -242,15 +237,15 @@ prop_Registry :: Actions RegState -> Property
 prop_Registry s =
   property $
     runIOSimProp $ do
-      -- _ <- run cleanUp
       monitor $ counterexample "\nExecution\n"
-      _res <- runPropertyIOSim (runActions runModelIOSim s) (error "don't look at uninitialized state")
+      _res <- runPropertyStateT (runActions s) (error "don't look at uninitialized state")
       assert True
 
--- cleanUp :: IO [Either ErrorCall ()]
--- cleanUp = sequence
---   [try (unregister name) :: IO (Either ErrorCall ())
---    | name <- allNames++["x"]]
+-- TODO: put this in some extras module
+runPropertyStateT :: Monad m => PropertyM (StateT s m) a -> s -> PropertyM m (a, s)
+runPropertyStateT p s0 = MkPropertyM $ \k -> do
+  m <- unPropertyM (do a <- p; s <- run get; return (a, s)) $ fmap lift . k
+  return $ evalStateT m s0
 
 propTest :: DynFormula RegState -> Property
 propTest d = forAllScripts d prop_Registry
@@ -292,13 +287,13 @@ canRegister s
   | length (regs s) == 5 = ignore -- all names are in use
   | null (tids s) = after Spawn canRegister
   | otherwise = forAllQ
-    ( elementsQ (allNames \\ map fst (regs s))
-    , elementsQ (tids s)
-    )
-    $ \(name, tid) ->
-      after
-        (Successful $ Register name tid)
-        done
+      ( elementsQ (allNames \\ map fst (regs s))
+      , elementsQ (tids s)
+      )
+      $ \(name, tid) ->
+        after
+          (Successful $ Register name tid)
+          done
 
 canRegisterName :: String -> RegState -> DynFormula RegState
 canRegisterName name s = forAllQ (elementsQ availableTids) $ \tid ->
@@ -310,29 +305,34 @@ canReregister :: RegState -> DynFormula RegState
 canReregister s
   | null (regs s) = ignore
   | otherwise = forAllQ (elementsQ $ map fst (regs s)) $ \name ->
-    after (Unregister name) (canRegisterName name)
+      after (Unregister name) (canRegisterName name)
 
 canRegisterName' :: String -> RegState -> DynFormula RegState
 canRegisterName' name s = forAllQ (elementsQ availableTids) $ \tid ->
   after (Successful $ Register name tid) done
  where
   availableTids = (tids s \\ map snd (regs s)) \\ dead s
 
-canReregister' :: Show (ThreadId (IOSim s)) => RegState -> DynFormula RegState
+canReregister' :: Show (IOClass.ThreadId (IOSim s)) => RegState -> DynFormula RegState
 canReregister' s
   | null (regs s) =
-    toStop $
-      if null availableTids
-        then after Spawn canReregister'
-        else after (Register "a" (head availableTids)) canReregister'
+      toStop $
+        if null availableTids
+          then after Spawn canReregister'
+          else after (Register "a" (head availableTids)) canReregister'
   | otherwise = forAllQ (elementsQ $ map fst (regs s)) $ \name ->
-    after (Unregister name) (canRegisterName' name)
+      after (Unregister name) (canRegisterName' name)
  where
   availableTids = (tids s \\ map snd (regs s)) \\ dead s
 
 tests :: TestTree
-tests =
-  testGroup
-    "registry model example"
-    -- TODO: fix property
-    [testProperty "prop_Registry" (property True)]
+tests = testGroup "registry model example" []
+
+-- TODO:
+--  * turn on this test
+--  * add DL properties
+{-
+testGroup
+  "registry model example"
+  [testProperty "prop_Registry" prop_Registry]
+-}

quickcheck-dynamic/CHANGELOG.md

@@ -19,3 +19,9 @@ changes.
 
 * Initial publication of quickcheck-dynamic library on Hackage
 * Provide base `StateModel` and `DynamicLogic` tools to write quickcheck-based models, express properties, and test them
+
+## 2.0.0
+
+* Add `Realized` type family to distinguish between the model- and real type of an action
+* Introduce `RunModel` type class for `perform`
+* Split `postcondition` and `monitoring` out from the `StateModel` to the `RunModel` type class