diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,19 @@ +#### 0.10.0 (2024-05-28) + +* Revert `WithSetup` variants that were introduced in 0.7.2. Due to the way + repetitions are done now, there is no need for these variants anymore (PR #43); + +* Delete `run[N]ParallelCommandsNTimes` in favor of the new + `forAll[N]ParallelCommandsNTimes` as repetitions now happen at the `forAll` + level (PR #43); + +* Rename `forall` to `forAll` as it will be a reserved word starting + in GHC 9.10.1 (see [GHC proposal 281](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst)) (PR #49); + +* Replace `ansi-wl-pprint` with `prettyprinter` because `ansi-wl-pprint` was + deprecated in favour of `prettyprinter` (PR #49). + + #### 0.9.0 (2024-01-16) * Split the package into the machinery that abstracts over whichever diffing diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -313,8 +313,6 @@ └──────────────────────────────────────────────┘ │ AnnotateC "Read" (PredicateC (1 :/= 2)) - -However, some repetitions of this sequence of commands passed. Maybe there is a race condition? ``` As we can see above, a mutable reference is first created, and then in @@ -380,12 +378,10 @@ times with the part of the generated list that doesn't belong to the prefix. - 2. initialize the state machine if necessary (see [this](#sut-initialization)); - - 3. execute the prefix sequentially as in the section above (checking pre- and + 2. execute the prefix sequentially as in the section above (checking pre- and post-conditions); - 4. execute the suffixes in parallel without checking pre/post-conditions + 3. execute the suffixes in parallel without checking pre/post-conditions and gather the trace (or history) of invocations and responses of each action; @@ -409,24 +405,24 @@ executed sequentially ``` - 5. if something goes wrong when executing the commands, shrink the generated + 4. if something goes wrong when executing the commands, shrink the generated commands and present a minimal counterexample; - 6. otherwise, try to find a possible sequential interleaving of action + 5. otherwise, try to find a possible sequential interleaving of action invocations and responses that respects the post-conditions. For each interleaving, this is done by advancing the `Concrete` model (starting at `initialModel`) through the sequence of pairs of invocations to `command Concrete` and the returned `response Concrete` emitted at step 3, and checking the post-condition for each pair. - 7. if no possible sequential interleaving was found, then shrink the generated + 6. if no possible sequential interleaving was found, then shrink the generated commands and present a minimal counterexample. The last two steps basically try to find a [linearisation](https://en.wikipedia.org/wiki/Linearizability) of calls that could have happend on a single thread. -Notice that step 6 above introduces a subtlety in the post-condition checks and +Notice that step 5 above introduces a subtlety in the post-condition checks and transitions for the `model Concrete`. Despite the system under test running in a concurrent way, the model can still be designed to work sequentially as *it will not be run in parallel*, it will only be advanced in a sequential way when @@ -435,116 +431,10 @@ As we cannot control the actual scheduling of the tasks, each sequence of commands (already fixed in a concrete prefix and a concrete list of suffixes) is -actually executed several times by default, i.e. steps 2 to 7 will be executed +actually executed several times by default, i.e. steps 2 to 6 will be executed multiple times for the same test case expecting that the scheduling of events varies between runs. One can further increase entropy by introducing random `threadDelay`s in the semantic function. - -#### Why is a parallel property failing? - -Unless in presence of more severe bugs, parallel properties can fail because of -mainly two reasons: a race condition is happening or a logic bug is present in -the code. Taking advantage of the fact that we are repeating multiple times each -sequence of commands, we can have some insight on which one of those cases seems -to be the cause. - -The parallel counterexample will show one of the following messages: - -- `However, some repetitions of this sequence of commands passed. Maybe there is - a race condition?`: In this case as some parallel executions of a given - sequence of commands have passed, it seems that the test outcome is being - affected by a race condition or a non-deterministic error. This message is - accurate in the sense that a logic bug will not result in some repetitions - succeeding. -- `And all repetitions of this sequence of commands failed. Maybe there is a - logic bug? Try with more repetitions to be sure that it happens consistently`: - In this case, one of two things can happen. Either there is a logic bug that - is triggered always (which is what the message suggest) or we were just super - unlucky (or super lucky, as we found an error) in this run and a race - condition manifested in all runs. In order to rule out this last case, one can - run the tests with more repetitions, which if the problem is that there is - indeed a race condition, should result in the other message being printed - instead. - -#### SUT initialization - -Some tests might require an environment that is used by the SUT to perform its -actions, for example some mutable variable. In these cases, the environment -should be isolated from other executions, and in parallel testing each sequence -of commands is executed several times as noted in the previous paragraph. The -way to ensure that the environment is not shared among those repetitions is by -defining the state machine inside a monadic action and use the -`runXCommandsXWithSetup` variants of the functions: - -``` haskell - -semantics :: Env -> Command Concrete -> m (Response Concrete) -semantics = ... - -sm :: m (StateMachine Model Command m Response) -sm = do - env <- initEnv {- initialize the environment -} - pure $ StateMachine { - ... - , QSM.semantics = semantics env - } - -smUnused :: StateMachine Model Command m Response -smUnused = StateMachine { - ... - , QSM.semantics = error "SUT must not be used during command generation or shrinking" -} - -prop = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ - prettyParallelCommands cmds =<< runParallelCommandsWithSetup sm cmds -``` - -This will ensure that each execution of the testcase initializes the environment -as a first step. - -Note however that when running **sequential properties**, each test case is only -executed once, therefore these two are completely equivalent: - -``` haskell -sm :: m (StateMachine Model Command m Response) -sm = do - env <- initEnv {- initialize the environment -} - pure $ StateMachine { - ... - , QSM.semantics = semantics env - } - -smUnused :: StateMachine Model Command m Response -smUnused = StateMachine { - ... - , QSM.semantics = error "SUT must not be used during command generation or shrinking" -} - -prop = forAllCommands smUnused $ \cmds -> monadicIO $ - (hist, _model, res) <- runCommandsWithSetup sm cmds - prettyCommands smUnused hist (checkCommandNames cmds (res === Ok)) -``` - -versus - -``` haskell -sm :: Env -> StateMachine Model Command m Response -sm env = StateMachine { - ... - , QSM.semantics = semantics env - } - -smUnused :: StateMachine Model Command m Response -smUnused = StateMachine { - ... - , QSM.semantics = error "SUT must not be used during command generation or shrinking" -} - -prop = forAllCommands smUnused $ \cmds -> monadicIO $ - env <- initEnv {- initialize the environment -} - (hist, _model, res) <- runCommands (sm env) cmds - prettyCommands smUnused hist (checkCommandNames cmds (res === Ok)) -``` ### More examples diff --git a/quickcheck-state-machine.cabal b/quickcheck-state-machine.cabal --- a/quickcheck-state-machine.cabal +++ b/quickcheck-state-machine.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: quickcheck-state-machine -version: 0.9.0 +version: 0.10.0 synopsis: Test monadic programs using state machine based models description: See README at @@ -23,7 +23,7 @@ README.md tested-with: - GHC ==8.8.4 || ==8.10.7 || ==9.2.8 || ==9.4.7 || ==9.6.3 || ==9.8.1 + GHC ==8.8.4 || ==8.10.7 || ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2 -- Due to `tree-diff` being `GPL`, this library makes use of an interface -- (@CanDiff@) to diff models. This can be implemented with the vendored @@ -70,14 +70,15 @@ , time >=1.7 && <1.13 build-depends: - , ansi-wl-pprint >=0.6.7.3 && <1.1 - , graphviz >=2999.20.0.3 && <2999.21 - , pretty-show >=1.6.16 && <1.11 - , QuickCheck >=2.12 && <2.15 - , random >=1.1 && <1.3 - , sop-core >=0.5.0.2 && <0.6 - , split >=0.2.3.5 && <0.3 - , unliftio >=0.2.7.0 && <0.3 + , graphviz >=2999.20.0.3 && <2999.21 + , pretty-show >=1.6.16 && <1.11 + , prettyprinter ^>=1.7.1 + , prettyprinter-ansi-terminal ^>=1.1.3 + , QuickCheck >=2.12 && <2.15 + , random >=1.1 && <1.3 + , sop-core >=0.5.0.2 && <0.6 + , split >=0.2.3.5 && <0.3 + , unliftio >=0.2.7.0 && <0.3 default-language: Haskell2010 @@ -124,7 +125,8 @@ , time build-depends: - , ansi-wl-pprint + , prettyprinter + , prettyprinter-ansi-terminal , QuickCheck , sop-core @@ -215,3 +217,8 @@ source-repository head type: git location: https://github.com/stevana/quickcheck-state-machine + +source-repository this + type: git + location: https://github.com/stevana/quickcheck-state-machine + tag: v0.10.0 diff --git a/src/Test/StateMachine.hs b/src/Test/StateMachine.hs --- a/src/Test/StateMachine.hs +++ b/src/Test/StateMachine.hs @@ -19,7 +19,6 @@ forAllCommands , existsCommands , runCommands - , runCommandsWithSetup , prettyCommands , prettyCommands' , checkCommandNames @@ -35,17 +34,12 @@ -- * Parallel property combinators , forAllParallelCommands , forAllNParallelCommands + , forAllParallelCommandsNTimes + , forAllNParallelCommandsNTimes , runNParallelCommands - , runNParallelCommandsWithSetup , runParallelCommands - , runParallelCommandsWithSetup , runParallelCommands' - , runParallelCommandsNTimes - , runParallelCommandsNTimesWithSetup - , runNParallelCommandsNTimes' - , runParallelCommandsNTimes' - , runNParallelCommandsNTimes - , runNParallelCommandsNTimesWithSetup + , runNParallelCommands' , prettyNParallelCommands , prettyParallelCommands , prettyParallelCommandsWithOpts diff --git a/src/Test/StateMachine/BoxDrawer.hs b/src/Test/StateMachine/BoxDrawer.hs --- a/src/Test/StateMachine/BoxDrawer.hs +++ b/src/Test/StateMachine/BoxDrawer.hs @@ -23,8 +23,8 @@ ) where import Prelude -import Text.PrettyPrint.ANSI.Leijen - (Doc, text, vsep) +import Prettyprinter + (Doc, pretty, vsep) import Test.StateMachine.Types (Pid(..)) @@ -99,8 +99,8 @@ deriving stock Functor -- | Given a history, and output from processes generate Doc with boxes -exec :: [(EventType, Pid)] -> Fork [String] -> Doc -exec evT (Fork lops pops rops) = vsep $ map text (preBoxes ++ parBoxes) +exec :: [(EventType, Pid)] -> Fork [String] -> Doc ann +exec evT (Fork lops pops rops) = vsep $ map pretty (preBoxes ++ parBoxes) where preBoxes = let pref = compilePrefix pops in map (adjust $ maximum $ map ((2+) . size) pref ++ map ((2+) . length) (take 1 parBoxes)) pref diff --git a/src/Test/StateMachine/ConstructorName.hs b/src/Test/StateMachine/ConstructorName.hs --- a/src/Test/StateMachine/ConstructorName.hs +++ b/src/Test/StateMachine/ConstructorName.hs @@ -19,9 +19,9 @@ import Data.Proxy (Proxy(Proxy)) import GHC.Generics - ((:*:)((:*:)), (:+:)(L1, R1), C, Constructor, D, - Generic1, K1, M1, Rec1, Rep1, S, U1, conName, from1, - unM1, unRec1) + (C, Constructor, D, Generic1, K1, M1, Rec1, Rep1, S, + U1, conName, from1, unM1, unRec1, (:*:)((:*:)), + (:+:)(L1, R1)) import Prelude import Test.StateMachine.Types diff --git a/src/Test/StateMachine/Diffing.hs b/src/Test/StateMachine/Diffing.hs --- a/src/Test/StateMachine/Diffing.hs +++ b/src/Test/StateMachine/Diffing.hs @@ -12,7 +12,8 @@ import Data.Proxy (Proxy(..)) -import qualified Text.PrettyPrint.ANSI.Leijen as WL +import qualified Prettyprinter as PP +import qualified Prettyprinter.Render.Terminal as PP class CanDiff x where -- | Expressions that will be diffed @@ -27,13 +28,13 @@ exprDiff :: Proxy x -> AnExpr x -> AnExpr x -> ADiff x -- | Output a diff in compact form - diffToDocCompact :: Proxy x -> ADiff x -> WL.Doc + diffToDocCompact :: Proxy x -> ADiff x -> PP.Doc PP.AnsiStyle -- | Output a diff - diffToDoc :: Proxy x -> ADiff x -> WL.Doc + diffToDoc :: Proxy x -> ADiff x -> PP.Doc PP.AnsiStyle -- | Output an expression - exprToDoc :: Proxy x -> AnExpr x -> WL.Doc + exprToDoc :: Proxy x -> AnExpr x -> PP.Doc PP.AnsiStyle ediff :: forall x. CanDiff x => x -> x -> ADiff x ediff x y = exprDiff (Proxy @x) (toDiff x) (toDiff y) diff --git a/src/Test/StateMachine/Logic.hs b/src/Test/StateMachine/Logic.hs --- a/src/Test/StateMachine/Logic.hs +++ b/src/Test/StateMachine/Logic.hs @@ -40,7 +40,7 @@ , (.&&) , (.||) , (.=>) - , forall + , forAll , exists ) where @@ -193,10 +193,10 @@ -- >>> gatherAnnotations (Bot .// "bot" .&& Top .// "top") -- [] -- --- >>> gatherAnnotations (forall [1,2,3] (\i -> 0 .< i .// "positive")) +-- >>> gatherAnnotations (forAll [1,2,3] (\i -> 0 .< i .// "positive")) -- ["positive","positive","positive"] -- --- >>> gatherAnnotations (forall [0,1,2,3] (\i -> 0 .< i .// "positive")) +-- >>> gatherAnnotations (forAll [0,1,2,3] (\i -> 0 .< i .// "positive")) -- [] -- -- >>> gatherAnnotations (exists [1,2,3] (\i -> 0 .< i .// "positive")) @@ -280,8 +280,8 @@ (.=>) :: Logic -> Logic -> Logic (.=>) = (:=>) -forall :: Show a => [a] -> (a -> Logic) -> Logic -forall = Forall +forAll :: Show a => [a] -> (a -> Logic) -> Logic +forAll = Forall exists :: Show a => [a] -> (a -> Logic) -> Logic exists = Exists diff --git a/src/Test/StateMachine/Parallel.hs b/src/Test/StateMachine/Parallel.hs --- a/src/Test/StateMachine/Parallel.hs +++ b/src/Test/StateMachine/Parallel.hs @@ -17,69 +17,52 @@ -- This module contains helpers for generating, shrinking, and checking -- parallel programs. -- --- Note that: --- --- - the @.*NParallelCommands@ functions and the 'NParallelCommands' datatype --- are expected to be used when you want to run @N@ concurrent threads running --- at the same time and repeat each test 10 (by default) times to get --- sufficient randomness on the RTS scheduling of concurrent actions. --- --- - the @.*ParallelCommandsNTimes@ functions and the 'ParallelCommands' --- datatype are expected to be used when you want to run the test with 2 --- concurrent threads and repeat each test @N@ times to get sufficient --- randomness on the RTS scheduling of concurrent actions. --- --- - the @.*NParallelCommandsNTime@ functions do both of the above points at the --- same time, in particular they take an 'NParallelCommands' value generated --- to be run by some number of threads concurrently, and they take as input --- how many times each test should be repeated. --- --- - the @run.*WithSetup@ functions receive a monadic action that must --- initialize the StateMachine which will be used at the beginning of each --- repetition of each sequence of commands. See the section in the --- [README](https://github.com/stevana/quickcheck-state-machine#sut-initialization) --- for more context. --- ----------------------------------------------------------------------------- module Test.StateMachine.Parallel - ( forAllNParallelCommands + ( -- forall + forAllNParallelCommands + , forAllNParallelCommandsNTimes + , forAllParallelCommandsNTimes , forAllParallelCommands + + -- generate , generateNParallelCommands , generateParallelCommands + + -- shrink , shrinkNParallelCommands , shrinkParallelCommands , shrinkAndValidateNParallel , shrinkAndValidateParallel , shrinkCommands' - , runNParallelCommands - , runNParallelCommandsWithSetup + + -- run , runParallelCommands - , runParallelCommandsWithSetup , runParallelCommands' - , runNParallelCommandsNTimes - , runNParallelCommandsNTimesWithSetup - , runParallelCommandsNTimes - , runParallelCommandsNTimesWithSetup - , runNParallelCommandsNTimes' - , runParallelCommandsNTimes' - , executeParallelCommands - , linearise - , toBoxDrawings + , runNParallelCommands + , runNParallelCommands' + + -- pretty , prettyNParallelCommands , prettyParallelCommands , prettyParallelCommandsWithOpts , prettyNParallelCommandsWithOpts + + -- misc , advanceModel , checkCommandNamesParallel , coverCommandNamesParallel , commandNamesParallel + , linearise + , toBoxDrawings + , executeParallelCommands ) where import Control.Monad - (replicateM, when) + (when) import Control.Monad.Catch - (MonadMask(..), ExitCase(..)) + (ExitCase(..), MonadMask, generalBracket) import Control.Monad.State.Strict (runStateT) import Data.Bifunctor @@ -87,7 +70,7 @@ import Data.Foldable (toList) import Data.List - (find, partition, permutations, foldl') + (find, foldl', partition, permutations) import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe, mapMaybe) @@ -98,20 +81,21 @@ import Data.Tree (Tree(Node)) import Prelude +import Prettyprinter + (Doc) import Test.QuickCheck (Gen, Property, Testable, choose, forAllShrinkShow, - property, sized) + property, sized, (.&&.)) import Test.QuickCheck.Monadic (PropertyM, run) -import Text.PrettyPrint.ANSI.Leijen - (Doc) import Text.Show.Pretty (ppShow) import UnliftIO - (MonadIO, MonadUnliftIO, concurrently, + (MonadIO, MonadUnliftIO, TChan, concurrently, forConcurrently, newTChanIO) -import qualified UnliftIO as UIO +import qualified Prettyprinter as PP +import qualified Prettyprinter.Render.Terminal as PP import Test.StateMachine.BoxDrawer import Test.StateMachine.ConstructorName import Test.StateMachine.DotDrawing @@ -120,10 +104,21 @@ import Test.StateMachine.Types import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Utils -import qualified Text.PrettyPrint.ANSI.Leijen as PP ------------------------------------------------------------------------ +forAllParallelCommandsNTimes :: Testable prop + => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) + => (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd m resp + -> Maybe Int + -> Int + -> (ParallelCommands cmd resp -> prop) -- ^ Predicate. + -> Property +forAllParallelCommandsNTimes sm mminSize reps prop = + forAllShrinkShow (generateParallelCommands sm mminSize) (shrinkParallelCommands sm) ppShow + (\parCmds -> foldl' (.&&.) (property True) $ replicate reps $ prop parCmds) + forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) @@ -132,8 +127,19 @@ -> (ParallelCommands cmd resp -> prop) -- ^ Predicate. -> Property forAllParallelCommands sm mminSize = - forAllShrinkShow (generateParallelCommands sm mminSize) (shrinkParallelCommands sm) ppShow + forAllParallelCommandsNTimes sm mminSize 10 +forAllNParallelCommandsNTimes :: Testable prop + => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) + => (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd m resp + -> Int -- ^ Number of threads + -> Int + -> (NParallelCommands cmd resp -> prop) -- ^ Predicate. + -> Property +forAllNParallelCommandsNTimes sm np reps prop = + forAllShrinkShow (generateNParallelCommands sm np) (shrinkNParallelCommands sm) ppShow + (\parCmds -> foldl' (.&&.) (property True) $ replicate reps $ prop parCmds) forAllNParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) @@ -143,8 +149,7 @@ -> (NParallelCommands cmd resp -> prop) -- ^ Predicate. -> Property forAllNParallelCommands sm np = - forAllShrinkShow (generateNParallelCommands sm np) (shrinkNParallelCommands sm) ppShow - + forAllNParallelCommandsNTimes sm np 10 -- | Generate parallel commands. -- @@ -498,170 +503,66 @@ ------------------------------------------------------------------------ runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => StateMachine model cmd m resp - -> ParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runParallelCommands = runParallelCommandsNTimes 10 - -runParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => m (StateMachine model cmd m resp) - -> ParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runParallelCommandsWithSetup = runParallelCommandsNTimesWithSetup 10 - -runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => m (StateMachine model cmd m resp) - -> (cmd Concrete -> resp Concrete) - -> ParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runParallelCommands' = runParallelCommandsNTimes' 10 - -runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => StateMachine model cmd m resp - -> NParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runNParallelCommands = runNParallelCommandsNTimes 10 - -runNParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => m (StateMachine model cmd m resp) - -> NParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runNParallelCommandsWithSetup = runNParallelCommandsNTimesWithSetup 10 - -runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) - => Int -- ^ How many times to execute the parallel program. - -> StateMachine model cmd m resp - -> ParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runParallelCommandsNTimes n sm = runParallelCommandsNTimesWithSetup n (pure sm) - -runParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => Int -- ^ How many times to execute the parallel program. - -> m (StateMachine model cmd m resp) + => StateMachine model cmd m resp -> ParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runParallelCommandsNTimesWithSetup n msm cmds = - replicateM n $ do + -> PropertyM m (History cmd resp, model Concrete, Logic) +runParallelCommands sm cmds = do hchan <- newTChanIO - ((hist, model, reason1, reason2), sm') <- run $ + ((hist, model, reason1, reason2), ()) <- run $ fst <$> generalBracket - msm - (\sm' ec -> case ec of - ExitCaseSuccess ((_, model, _, _), _) -> cleanup sm' model - _ -> getChanContents hchan >>= cleanup sm' . mkModel sm' . History + (pure ()) + (\_ ec -> case ec of + ExitCaseSuccess ((_, model, _, _), _) -> cleanup sm model + _ -> getChanContents hchan >>= cleanup sm . mkModel sm . History ) - (\sm' -> (,sm') <$> executeParallelCommands sm' cmds hchan True) - return (hist, model, logicReason (combineReasons [reason1, reason2]) .&& linearise sm' hist) + (\_ -> (,()) <$> executeParallelCommands sm cmds hchan True) + return (hist, model, logicReason (combineReasons [reason1, reason2]) .&& linearise sm hist) -runParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) +runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) - => Int -- ^ How many times to execute the parallel program. - -> m (StateMachine model cmd m resp) + => StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runParallelCommandsNTimes' n msm complete cmds = - replicateM n $ do - hchan <- newTChanIO - ((hist, model, _, _), sm') <- run $ - fst <$> generalBracket - msm - (\sm' ec -> case ec of - ExitCaseSuccess ((_, model, _, _), _) -> cleanup sm' model - _ -> getChanContents hchan >>= cleanup sm' . mkModel sm' . History - ) - (\sm' -> (,sm') <$> executeParallelCommands sm' cmds hchan True) - let hist' = completeHistory complete hist - return (hist', model, linearise sm' hist') - - -runNParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => Int -- ^ How many times to execute the parallel program. - -> StateMachine model cmd m resp - -> NParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runNParallelCommandsNTimes n sm = runNParallelCommandsNTimesWithSetup n (pure sm) - -runNParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => Int -- ^ How many times to execute the parallel program. - -> m (StateMachine model cmd m resp) - -> NParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runNParallelCommandsNTimesWithSetup n msm cmds = - replicateM n $ do - hchan <- newTChanIO - ((hist, model, reason), sm') <- run $ - fst <$> generalBracket - msm - (\sm' ec -> case ec of - ExitCaseSuccess ((_, model, _), _) -> cleanup sm' model - _ -> getChanContents hchan >>= cleanup sm' . mkModel sm' . History - ) - (\sm' -> (,sm') <$> executeNParallelCommands sm' cmds hchan True) - return (hist, model, logicReason reason .&& linearise sm' hist) - -runNParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadUnliftIO m) - => Int -- ^ How many times to execute the parallel program. - -> m (StateMachine model cmd m resp) - -> (cmd Concrete -> resp Concrete) - -> NParallelCommands cmd resp - -> PropertyM m [(History cmd resp, model Concrete, Logic)] -runNParallelCommandsNTimes' n msm complete cmds = - replicateM n $ do + -> PropertyM m (History cmd resp, model Concrete, Logic) +runParallelCommands' sm complete cmds = do hchan <- newTChanIO - ((hist, model, _reason), sm') <- run $ + ((hist, model, _reason1, _reason2), ()) <- run $ fst <$> generalBracket - msm - (\sm' ec -> case ec of - ExitCaseSuccess ((_, model, _), _) -> cleanup sm' model - _ -> getChanContents hchan >>= cleanup sm' . mkModel sm' . History + (pure ()) + (\_ ec -> case ec of + ExitCaseSuccess ((_, model, _, _), _) -> cleanup sm model + _ -> getChanContents hchan >>= cleanup sm . mkModel sm . History ) - (\sm' -> (,sm') <$> executeNParallelCommands sm' cmds hchan True) + (\_ -> (,()) <$> executeParallelCommands sm cmds hchan True) let hist' = completeHistory complete hist - return (hist, model, linearise sm' hist') + return (hist', model, linearise sm hist') executeParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp - -> UIO.TChan (Pid, HistoryEvent cmd resp) + -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) executeParallelCommands sm@StateMachine{ initModel } (ParallelCommands prefix suffixes) hchan stopOnError = do - - (reason0, (env0, _smodel, _counter, cmodel)) <- runStateT - (executeCommands sm hchan (Pid 0) CheckEverything prefix) - (emptyEnvironment, initModel, newCounter, initModel) - if reason0 /= Ok - then do - hist <- getChanContents hchan - return (History hist, cmodel, reason0, reason0) - else do - (reason1, reason2, _) <- go (Ok, Ok, env0) suffixes - hist <- getChanContents hchan - return (History hist, cmodel, reason1, reason2) + (reason0, (env0, _smodel, _counter, _cmodel)) <- + runStateT + (executeCommands sm hchan (Pid 0) CheckEverything prefix) + (emptyEnvironment, initModel, newCounter, initModel) + if reason0 /= Ok + then do + hist <- getChanContents hchan + let model = mkModel sm $ History hist + return (History hist, model, reason0, reason0) + else do + (reason1, reason2, _) <- go (Ok, Ok, env0) suffixes + hist <- getChanContents hchan + let model = mkModel sm $ History hist + return (History hist, model, reason1, reason2) where go (res1, res2, env) [] = return (res1, res2, env) go (Ok, Ok, env) (Pair cmds1 cmds2 : pairs) = do @@ -723,26 +624,67 @@ logicReason Ok = Top logicReason r = Annotate (show r) Bot +runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) + => (Rank2.Traversable cmd, Rank2.Foldable resp) + => (MonadMask m, MonadUnliftIO m) + => StateMachine model cmd m resp + -> NParallelCommands cmd resp + -> PropertyM m (History cmd resp, model Concrete, Logic) +runNParallelCommands sm cmds = do + hchan <- newTChanIO + ((hist, model, reason), ()) <- run $ + fst <$> generalBracket + (pure ()) + (\_ ec -> case ec of + ExitCaseSuccess ((_, model, _), _) -> cleanup sm model + _ -> getChanContents hchan >>= cleanup sm . mkModel sm . History + ) + (\_ -> (,()) <$> executeNParallelCommands sm cmds hchan True) + return (hist, model, logicReason reason .&& linearise sm hist) + +runNParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) + => (Rank2.Traversable cmd, Rank2.Foldable resp) + => (MonadMask m, MonadUnliftIO m) + => StateMachine model cmd m resp + -> (cmd Concrete -> resp Concrete) + -> NParallelCommands cmd resp + -> PropertyM m (History cmd resp, model Concrete, Logic) +runNParallelCommands' sm complete cmds = do + hchan <- newTChanIO + ((hist, model, _reason), ()) <- run $ + fst <$> generalBracket + (pure ()) + (\_ ec -> case ec of + ExitCaseSuccess ((_, model, _), _) -> cleanup sm model + _ -> getChanContents hchan >>= cleanup sm . mkModel sm . History + ) + (\_ -> (,()) <$> executeNParallelCommands sm cmds hchan True) + let hist' = completeHistory complete hist + return (hist, model, linearise sm hist') + executeNParallelCommands :: (Rank2.Traversable cmd, Show (cmd Concrete), Rank2.Foldable resp) => Show (resp Concrete) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp - -> UIO.TChan (Pid, HistoryEvent cmd resp) + -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason) executeNParallelCommands sm@StateMachine{ initModel } (ParallelCommands prefix suffixes) hchan stopOnError = do - (reason0, (env0, _smodel, _counter, cmodel)) <- runStateT - (executeCommands sm hchan (Pid 0) CheckEverything prefix) - (emptyEnvironment, initModel, newCounter, initModel) - if reason0 /= Ok - then do - hist <- getChanContents hchan - return (History hist, cmodel, reason0) - else do - (errors, _) <- go (Map.empty, env0) suffixes - hist <- getChanContents hchan - return (History hist, cmodel, combineReasons $ Map.elems errors) + (reason0, (env0, _smodel, _counter, _cmodel)) <- + runStateT + (executeCommands sm hchan (Pid 0) CheckEverything prefix) + (emptyEnvironment, initModel, newCounter, initModel) + if reason0 /= Ok + then do + hist <- getChanContents hchan + let model = mkModel sm $ History hist + return (History hist, model, reason0) + else do + (errors, _) <- go (Map.empty, env0) suffixes + hist <- getChanContents hchan + let model = mkModel sm $ History hist + return (History hist, model, combineReasons $ Map.elems errors) where go res [] = return res go (previousErrors, env) (suffix : rest) = do @@ -810,23 +752,17 @@ => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions - -> [(History cmd resp, a, Logic)] -- ^ Output of 'runParallelCommands'. + -> (History cmd resp, model Concrete, Logic) -- ^ Output of 'runParallelCommands'. -> PropertyM m () -prettyParallelCommandsWithOpts cmds mGraphOptions histories = do - mapM_ (\(h, _, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l)) histories +prettyParallelCommandsWithOpts cmds mGraphOptions (h, _, l) = do + printCounterexample h (logic l) `whenFailM` property (boolean l) where printCounterexample hist' (VFalse ce) = do PP.putDoc $ mconcat [ PP.line - , PP.string (show $ toBoxDrawings cmds hist') - , PP.string (show $ simplify ce) - , PP.line - , PP.line - , PP.string $ - if or [ boolean l | (_, _, l) <- histories] - then "However, some repetitions of this sequence of commands passed. Maybe there is a race condition?" - else "And all repetitions of this sequence of commands failed. Maybe there is a logic bug? Try with more repetitions to be sure that it happens consistently" + , PP.pretty (show $ toBoxDrawings cmds hist') + , PP.pretty (show $ simplify ce) , PP.line ] case mGraphOptions of @@ -842,14 +778,14 @@ simplify (ExistsC _ [Fst ce]) = ce simplify (ExistsC x (Fst ce : ces)) = ce `EitherC` simplify (ExistsC x ces) simplify (ExistsC _ (Snd ce : _)) = simplify ce -simplify _ = error "simplify: impossible,\ - \ because of the structure of linearise." +simplify _ = error "simplify: impossible, \ + \because of the structure of linearise." prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Rank2.Foldable cmd => ParallelCommands cmd resp - -> [(History cmd resp, a, Logic)] -- ^ Output of 'runNParallelCommands'. + -> (History cmd resp, model Concrete, Logic) -- ^ Output of 'runParallelCommands'. -> PropertyM m () prettyParallelCommands cmds = prettyParallelCommandsWithOpts cmds Nothing @@ -860,22 +796,16 @@ => Rank2.Foldable cmd => NParallelCommands cmd resp -> Maybe GraphOptions - -> [(History cmd resp, a, Logic)] -- ^ Output of 'runNParallelCommands'. + -> (History cmd resp, model Concrete, Logic) -- ^ Output of 'runNParallelCommands'. -> PropertyM m () -prettyNParallelCommandsWithOpts cmds mGraphOptions histories = - mapM_ (\(h, _, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l)) histories +prettyNParallelCommandsWithOpts cmds mGraphOptions (h, _, l) = + printCounterexample h (logic l) `whenFailM` property (boolean l) where printCounterexample hist' (VFalse ce) = do PP.putDoc $ mconcat [ PP.line - , PP.string (show $ simplify ce) - , PP.line - , PP.line - , PP.string $ - if or [ boolean l | (_, _, l) <- histories] - then "However, some repetitions of this sequence of commands passed. Maybe there is a race condition?" - else "And all repetitions of this sequence of commands failed. Maybe there is a logic bug? Try with more repetitions to be sure that it happens consistently" + , PP.pretty (show $ simplify ce) , PP.line ] case mGraphOptions of @@ -888,21 +818,21 @@ => MonadIO m => Rank2.Foldable cmd => NParallelCommands cmd resp - -> [(History cmd resp, a, Logic)] -- ^ Output of 'runNParallelCommands'. + -> (History cmd resp, model Concrete, Logic) -- ^ Output of 'runNParallelCommands'. -> PropertyM m () prettyNParallelCommands cmds = prettyNParallelCommandsWithOpts cmds Nothing -- | Draw an ASCII diagram of the history of a parallel program. Useful for -- seeing how a race condition might have occured. -toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd +toBoxDrawings :: forall cmd resp ann. Rank2.Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) - => ParallelCommands cmd resp -> History cmd resp -> Doc + => ParallelCommands cmd resp -> History cmd resp -> Doc ann toBoxDrawings (ParallelCommands prefix suffixes) = toBoxDrawings'' allVars where allVars = getAllUsedVars prefix `S.union` foldMap (foldMap getAllUsedVars) suffixes - toBoxDrawings'' :: Set Var -> History cmd resp -> Doc + toBoxDrawings'' :: Set Var -> History cmd resp -> Doc ann toBoxDrawings'' knownVars (History h) = mconcat ([ exec evT (fmap (out . snd) <$> Fork l p r) , PP.line @@ -940,11 +870,11 @@ evT :: [(EventType, Pid)] evT = toEventType (filter (\e -> fst e `Prelude.elem` map Pid [1, 2]) h) - ppException :: (Int, String) -> Doc + ppException :: (Int, String) -> Doc ann ppException (idx, err) = mconcat - [ PP.string $ "Exception " <> show idx <> ":" + [ PP.pretty $ "Exception " <> show idx <> ":" , PP.line - , PP.indent 2 $ PP.string err + , PP.indent 2 $ PP.pretty err , PP.line , PP.line ] diff --git a/src/Test/StateMachine/Sequential.hs b/src/Test/StateMachine/Sequential.hs --- a/src/Test/StateMachine/Sequential.hs +++ b/src/Test/StateMachine/Sequential.hs @@ -37,7 +37,6 @@ , ShouldShrink(..) , initValidateEnv , runCommands - , runCommandsWithSetup , runCommands' , getChanContents , Check(..) @@ -63,7 +62,8 @@ import Control.Monad (when) import Control.Monad.Catch - (ExitCase(..), MonadCatch(..), MonadMask(..), catch) + (ExitCase(..), MonadCatch, MonadMask, catch, + generalBracket) import Control.Monad.State.Strict (StateT, evalStateT, get, lift, put, runStateT) import Data.Bifunctor @@ -86,6 +86,10 @@ import Data.Time (defaultTimeLocale, formatTime, getZonedTime) import Prelude +import Prettyprinter + (Doc) +import qualified Prettyprinter as PP +import qualified Prettyprinter.Render.Terminal as PP import System.Directory (createDirectoryIfMissing) import System.FilePath @@ -101,9 +105,6 @@ (PropertyM, run) import Test.QuickCheck.Random (mkQCGen) -import qualified Text.PrettyPrint.ANSI.Leijen as PP -import Text.PrettyPrint.ANSI.Leijen - (Doc) import Text.Show.Pretty (ppShow) import UnliftIO @@ -330,36 +331,28 @@ => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) -runCommands sm = runCommandsWithSetup (pure sm) - -runCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) - => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadMask m, MonadIO m) - => m (StateMachine model cmd m resp) - -> Commands cmd resp - -> PropertyM m (History cmd resp, model Concrete, Reason) -runCommandsWithSetup msm cmds = run $ runCommands' msm cmds +runCommands sm cmds = run $ runCommands' sm cmds runCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadIO m) - => m (StateMachine model cmd m resp) + => StateMachine model cmd m resp -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason) -runCommands' msm cmds = do - hchan <- newTChanIO - (reason, (_, _, _, model)) <- - fst <$> generalBracket - msm - (\sm' ec -> case ec of - ExitCaseSuccess (_, (_,_,_,model)) -> cleanup sm' model - _ -> getChanContents hchan >>= cleanup sm' . mkModel sm' . History - ) - (\sm'@StateMachine{ initModel } -> runStateT - (executeCommands sm' hchan (Pid 0) CheckEverything cmds) - (emptyEnvironment, initModel, newCounter, initModel)) - hist <- getChanContents hchan - return (History hist, model, reason) +runCommands' sm@StateMachine { initModel, cleanup } cmds = do + hchan <- newTChanIO + (reason, (_, _, _, model)) <- fst <$> generalBracket + (pure ()) + (\_ ec -> case ec of + ExitCaseSuccess (_, (_, _, _, model)) -> cleanup model + _ -> getChanContents hchan >>= cleanup . mkModel sm . History) + (\_ -> do + runStateT + (executeCommands sm hchan (Pid 0) CheckEverything cmds) + (emptyEnvironment, initModel, newCounter, initModel) + ) + hist <- getChanContents hchan + return (History hist, model, reason) -- We should try our best to not let this function fail, -- since it is used to cleanup resources, in parallel programs. @@ -464,7 +457,7 @@ getUsedConcrete :: Rank2.Foldable f => f Concrete -> [Dynamic] getUsedConcrete = Rank2.foldMap (\(Concrete x) -> [toDyn x]) -modelDiff :: forall model r. CanDiff (model r) => model r -> Maybe (model r) -> Doc +modelDiff :: forall model r. CanDiff (model r) => model r -> Maybe (model r) -> Doc PP.AnsiStyle modelDiff model = diffToDocCompact p . flip ediff model . fromMaybe model where p = Proxy @(model r) @@ -480,7 +473,7 @@ . makeOperations . unHistory where - go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc + go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc PP.AnsiStyle go current previous [] = PP.line <> modelDiff current previous <> PP.line <> PP.line go current previous [Crash cmd err pid] = @@ -488,13 +481,13 @@ [ PP.line , modelDiff current previous , PP.line, PP.line - , PP.string " == " - , PP.string (ppShow cmd) - , PP.string " ==> " - , PP.string err - , PP.string " [ " - , PP.int (unPid pid) - , PP.string " ]" + , PP.pretty " == " + , PP.pretty (ppShow cmd) + , PP.pretty " ==> " + , PP.pretty err + , PP.pretty " [ " + , PP.pretty (unPid pid) + , PP.pretty " ]" , PP.line ] go current previous (Operation cmd resp pid : ops) = @@ -502,13 +495,13 @@ [ PP.line , modelDiff current previous , PP.line, PP.line - , PP.string " == " - , PP.string (ppShow cmd) - , PP.string " ==> " - , PP.string (ppShow resp) - , PP.string " [ " - , PP.int (unPid pid) - , PP.string " ]" + , PP.pretty " == " + , PP.pretty (ppShow cmd) + , PP.pretty " ==> " + , PP.pretty (ppShow resp) + , PP.pretty " [ " + , PP.pretty (unPid pid) + , PP.pretty " ]" , PP.line , go (transition current cmd resp) (Just current) ops ] @@ -535,11 +528,11 @@ . makeOperations . unHistory where - tagsDiff :: [tag] -> [tag] -> Doc + tagsDiff :: [tag] -> [tag] -> Doc PP.AnsiStyle tagsDiff old new = diffToDocCompact (Proxy @[tag]) (ediff old new) go :: model Concrete -> Maybe (model Concrete) -> [tag] -> [[tag]] - -> [Operation cmd resp] -> Doc + -> [Operation cmd resp] -> Doc PP.AnsiStyle go current previous _seen _tags [] = PP.line <> modelDiff current previous <> PP.line <> PP.line go current previous seen (tags : _) [Crash cmd err pid] = @@ -547,34 +540,34 @@ [ PP.line , modelDiff current previous , PP.line, PP.line - , PP.string " == " - , PP.string (ppShow cmd) - , PP.string " ==> " - , PP.string err - , PP.string " [ " - , PP.int (unPid pid) - , PP.string " ]" + , PP.pretty " == " + , PP.pretty (ppShow cmd) + , PP.pretty " ==> " + , PP.pretty err + , PP.pretty " [ " + , PP.pretty (unPid pid) + , PP.pretty " ]" , PP.line , if not (null tags) - then PP.line <> PP.string " " <> tagsDiff seen tags <> PP.line - else PP.empty + then PP.line <> PP.pretty " " <> tagsDiff seen tags <> PP.line + else PP.emptyDoc ] go current previous seen (tags : tagss) (Operation cmd resp pid : ops) = mconcat [ PP.line , modelDiff current previous , PP.line, PP.line - , PP.string " == " - , PP.string (ppShow cmd) - , PP.string " ==> " - , PP.string (ppShow resp) - , PP.string " [ " - , PP.int (unPid pid) - , PP.string " ]" + , PP.pretty " == " + , PP.pretty (ppShow cmd) + , PP.pretty " ==> " + , PP.pretty (ppShow resp) + , PP.pretty " [ " + , PP.pretty (unPid pid) + , PP.pretty " ]" , PP.line , if not (null tags) - then PP.line <> PP.string " " <> tagsDiff seen tags <> PP.line - else PP.empty + then PP.line <> PP.pretty " " <> tagsDiff seen tags <> PP.line + else PP.emptyDoc , go (transition current cmd resp) (Just current) tags tagss ops ] go _ _ _ _ _ = error "prettyPrintHistory': impossible." diff --git a/src/Test/StateMachine/Types/Rank2.hs b/src/Test/StateMachine/Types/Rank2.hs --- a/src/Test/StateMachine/Types/Rank2.hs +++ b/src/Test/StateMachine/Types/Rank2.hs @@ -25,8 +25,9 @@ (Type) import qualified Data.Traversable as Rank1 import GHC.Generics - ((:*:)((:*:)), (:+:)(L1, R1), Generic1, K1(K1), - M1(M1), Rec1(Rec1), Rep1, U1(U1), from1, to1, (:.:)(Comp1)) + (Generic1, K1(K1), M1(M1), Rec1(Rec1), Rep1, U1(U1), + from1, to1, (:*:)((:*:)), (:+:)(L1, R1), + (:.:)(Comp1)) import Prelude hiding (Applicative(..), Foldable(..), Functor(..), Traversable(..), (<$>)) diff --git a/src/Test/StateMachine/Utils.hs b/src/Test/StateMachine/Utils.hs --- a/src/Test/StateMachine/Utils.hs +++ b/src/Test/StateMachine/Utils.hs @@ -41,7 +41,8 @@ import Prelude -import Data.Bifunctor (second) +import Data.Bifunctor + (second) import Data.List (foldl') import Test.QuickCheck diff --git a/test/Cleanup.hs b/test/Cleanup.hs --- a/test/Cleanup.hs +++ b/test/Cleanup.hs @@ -39,11 +39,9 @@ import System.Random import Test.QuickCheck import Test.QuickCheck.Monadic - (monadicIO) + (monadicIO, run) import Test.StateMachine import Test.StateMachine.TreeDiff -import qualified Test.StateMachine.Types as QSM - (initModel) import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Utils (liftProperty, mkModel, whenFailM) @@ -92,14 +90,13 @@ , semanticsCounter :: Opaque (MVar Int) , ref :: Opaque (MVar Int) , value :: Int - , modelTestDir :: String } deriving stock (Generic, Show, Eq) instance ToExpr (Model Symbolic) instance ToExpr (Model Concrete) -initModel :: MVar Int -> MVar Int -> String -> Model r +initModel :: MVar Int -> MVar Int -> Model r initModel sc ref = Model Map.empty 0 (Opaque sc) (Opaque ref) 0 transition :: Ord1 r => Model r -> Command r -> Response r -> Model r @@ -139,7 +136,7 @@ removeFileRef dc (MVarC r _) = modifyMVar_ r $ \(file, isHere) -> do case (isHere, dc) of (_, ReDo) -> removeFile file - (True, _) -> removeFile file + (True, NoOp) -> removeFile file (False, NoOp) -> return () return (file, False) @@ -201,63 +198,71 @@ shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic] shrinker _ _ = [] -cleanup :: DoubleCleanup -> Model Concrete -> IO () -cleanup dc Model{..} = do +cleanup :: String -> DoubleCleanup -> Model Concrete -> IO () +cleanup testDir dc Model{..} = do let cl = do forM_ (Map.keys files) $ \rf -> removeFileRef dc $ unOpaque $ concrete rf modifyMVar_ (unOpaque semanticsCounter) (\_ -> return 0) modifyMVar_ (unOpaque ref) (\_ -> return 0) - cl `finally` removePathForcibly modelTestDir + -- onException here does not affect any tests. It just makes sure + -- no leftover directories remain after the end of tests. + -- We have it here, because we found no other way to handle the + -- exceptions in the PropertyM level. + cl `onException` removePathForcibly testDir -sm :: MVar Int -> MVar Int -> Bug -> DoubleCleanup -> IO (StateMachine Model Command IO Response) -sm counter ref bug dc = do - folderId :: Word <- randomIO - let testDir = testDirectoryBase ++ "-" ++ show folderId - exist <- doesDirectoryExist testDir - when exist $ removePathForcibly testDir - createDirectory testDir - pure $ StateMachine (initModel counter ref testDir) transition precondition postcondition - Nothing generator shrinker (semantics counter ref testDir bug) mock (cleanup dc) +sm :: MVar Int -> MVar Int -> String -> Bug -> DoubleCleanup -> StateMachine Model Command IO Response +sm counter ref tstDir bug dc = StateMachine (initModel counter ref) transition precondition postcondition + Nothing generator shrinker (semantics counter ref tstDir bug) mock (cleanup tstDir dc) smUnused :: StateMachine Model Command IO Response -smUnused = StateMachine (initModel f e "generator") transition precondition postcondition - Nothing generator shrinker (semantics e e e e) mock (cleanup e) - where - e = error "SUT must not be used" - f = error "SUT must not be useddd" +smUnused = sm e e e e e + where + e = error "SUT must not be used" +mkEnv :: MonadIO m + => Bug + -> DoubleCleanup + -> m (StateMachine Model Command IO Response, [Char]) +mkEnv bug dc = do + -- ideally this would use System.IO.Temp.withTempDirectory + -- but it is not possible at the moment, see: + -- https://github.com/hedgehogqa/haskell-hedgehog/issues/182 + folderId :: Word <- liftIO randomIO + let testDir = testDirectoryBase ++ "-" ++ show folderId + liftIO $ do + removePathForcibly testDir + createDirectory testDir + c <- liftIO $ newMVar 0 + ref <- liftIO $ newMVar 0 + let sm' = sm c ref testDir bug dc + pure (sm', testDir) + prop_sequential_clean :: FinalTest -> Bug -> DoubleCleanup -> Property prop_sequential_clean testing bug dc = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do - counter <- liftIO $ newMVar 0 - ref <- liftIO $ newMVar 0 - let sm' = sm counter ref bug dc - (hist, model, res) <- runCommandsWithSetup sm' cmds + (sm', testDir) <- run $ mkEnv bug dc + (hist, model, res) <- runCommands sm' cmds + ls <- liftIO $ listDirectory testDir + liftIO $ removePathForcibly testDir case testing of - Regular -> prettyCommands smUnused hist $ checkCommandNames cmds (res === Ok) - Files -> do - ex <- property . not <$> (liftIO $ doesDirectoryExist $ modelTestDir model) - (do - ls <- liftIO $ listDirectory $ modelTestDir model - printFiles ls) `whenFailM` ex - Eq _ -> liftProperty $ mkModel smUnused { QSM.initModel = initModel counter ref (modelTestDir model) } hist === model + Regular -> prettyCommands smUnused hist $ checkCommandNames cmds (res === Ok) + Files -> printFiles ls `whenFailM` (ls === []) + Eq _ -> liftProperty $ mkModel sm' hist === model prop_parallel_clean :: FinalTest -> Bug -> DoubleCleanup -> Property prop_parallel_clean testing bug dc = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do - counter <- liftIO $ newMVar 0 - ref <- liftIO $ newMVar 0 - let sm' = sm counter ref bug dc - ret <- runParallelCommandsNTimesWithSetup 2 sm' cmds + [(ret1, ls1), (ret2, ls2)] <- + replicateM 2 $ do + (sm', testDir) <- run $ mkEnv bug dc + ret <- runParallelCommands sm' cmds + ls <- liftIO $ listDirectory testDir + liftIO $ removePathForcibly testDir + pure (ret, ls) case testing of - Regular -> prettyParallelCommands cmds ret - Files -> - mapM_ (\(_, model, _) -> do - ex <- property . not <$> (liftIO $ doesDirectoryExist $ modelTestDir model) - (do - ls <- liftIO $ listDirectory $ modelTestDir model - printFiles ls) `whenFailM` ex) ret + Regular -> prettyParallelCommands cmds ret1 >> prettyParallelCommands cmds ret2 + Files -> mapM_ (\l -> printFiles l `whenFailM` (l === [])) [ls1, ls2] Eq bl -> do - let (a, b) = case mkModel smUnused . (\(h, _, _) -> h) <$> ret of + let (a, b) = case mkModel smUnused . (\(h, _, _) -> h) <$> [ret1, ret2] of (x : y : _) -> (x,y) _ -> error "expected at least two histories" liftProperty $ printModels a b `whenFail` @@ -265,20 +270,19 @@ prop_nparallel_clean :: Int -> FinalTest -> Bug -> DoubleCleanup -> Property prop_nparallel_clean np testing bug dc = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do - counter <- liftIO $ newMVar 0 - ref <- liftIO $ newMVar 0 - let sm' = sm counter ref bug dc - ret <- runNParallelCommandsNTimesWithSetup 2 sm' cmds -- This 2 is there just to have two histories later on! + [(ret1, ls1), (ret2, ls2)] <- + replicateM 2 $ do + (sm', testDir) <- run $ mkEnv bug dc + ret <- runNParallelCommands sm' cmds + ls <- liftIO $ listDirectory testDir + liftIO $ removePathForcibly testDir + pure (ret, ls) + case testing of - Regular -> prettyNParallelCommands cmds ret - Files -> - mapM_ (\(_, model, _) -> do - ex <- property . not <$> (liftIO $ doesDirectoryExist $ modelTestDir model) - (do - ls <- liftIO $ listDirectory $ modelTestDir model - printFiles ls) `whenFailM` ex) ret + Regular -> mapM_ (prettyNParallelCommands cmds) [ret1, ret2] + Files -> mapM_ (\l -> printFiles l `whenFailM` (l === [])) [ls1, ls2] Eq bl -> do - let (a, b) = case mkModel smUnused . (\(h, _, _) -> h) <$> ret of + let (a, b) = case mkModel smUnused . (\(h, _, _) -> h) <$> [ret1, ret2] of (x : y : _) -> (x,y) _ -> error "expected at least two histories" liftProperty $ printModels a b `whenFail` diff --git a/test/CrudWebserverDb.hs b/test/CrudWebserverDb.hs --- a/test/CrudWebserverDb.hs +++ b/test/CrudWebserverDb.hs @@ -386,8 +386,8 @@ prop_crudWebserverDbParallel :: Int -> Property prop_crudWebserverDbParallel port = - forAllParallelCommands sm Nothing $ \cmds -> monadic (ioProperty . runner port) $ - prettyParallelCommands cmds =<< runParallelCommandsNTimes 30 sm cmds + forAllParallelCommandsNTimes sm Nothing 30 $ \cmds -> monadic (ioProperty . runner port) $ + prettyParallelCommands cmds =<< runParallelCommands sm cmds demoRace' :: Int -> IO () demoRace' port = withCrudWebserverDb Race port diff --git a/test/Echo.hs b/test/Echo.hs --- a/test/Echo.hs +++ b/test/Echo.hs @@ -36,7 +36,8 @@ import Test.QuickCheck.Monadic (monadicIO) import UnliftIO - (TVar, atomically, newTVarIO, readTVar, writeTVar) + (TVar, atomically, liftIO, newTVarIO, readTVar, + writeTVar) import Test.StateMachine import Test.StateMachine.TreeDiff @@ -76,97 +77,88 @@ prop_echoOK :: Property prop_echoOK = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do - (hist, _, res) <- runCommandsWithSetup echoSM cmds - prettyCommands smUnused hist (res === Ok) + env <- liftIO $ mkEnv + let echoSM' = echoSM env + (hist, _, res) <- runCommands echoSM' cmds + prettyCommands echoSM' hist (res === Ok) prop_echoParallelOK :: Property prop_echoParallelOK = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do - prettyParallelCommands cmds =<< runParallelCommandsWithSetup echoSM cmds + env <- liftIO $ mkEnv + let echoSM' = echoSM env + prettyParallelCommands cmds =<< runParallelCommands echoSM' cmds prop_echoNParallelOK :: Int -> Property prop_echoNParallelOK np = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do - prettyNParallelCommands cmds =<< runNParallelCommandsWithSetup echoSM cmds + env <- liftIO $ mkEnv + let echoSM' = echoSM env + prettyNParallelCommands cmds =<< runNParallelCommands echoSM' cmds smUnused :: StateMachine Model Action IO Response -smUnused = StateMachine - { initModel = Empty -- At the beginning of time nothing was received. - , transition = transitions - , precondition = preconditions - , postcondition = postconditions - , QC.generator = Echo.generator - , invariant = Nothing - , QC.shrinker = Echo.shrinker - , QC.semantics = e - , QC.mock = Echo.mock - , cleanup = noCleanup - } - where - e = error "SUT must not be used" +smUnused = echoSM $ error "used env during command generation" -echoSM :: IO (StateMachine Model Action IO Response) -echoSM = do - env <- mkEnv - pure $ StateMachine +echoSM :: Env -> StateMachine Model Action IO Response +echoSM env = StateMachine { initModel = Empty -- At the beginning of time nothing was received. - , transition = transitions - , precondition = preconditions - , postcondition = postconditions - , QC.generator = Echo.generator + , transition = mTransitions + , precondition = mPreconditions + , postcondition = mPostconditions + , generator = mGenerator , invariant = Nothing - , QC.shrinker = Echo.shrinker - , QC.semantics = Echo.semantics env - , QC.mock = Echo.mock + , shrinker = mShrinker + , semantics = mSemantics + , mock = mMock , cleanup = noCleanup } - -transitions :: Model r -> Action r -> Response r -> Model r -transitions Empty (In str) _ = Buf str -transitions (Buf _) Echo _ = Empty -transitions Empty Echo _ = Empty --- TODO: qcsm will match the case below. However we don't expect this to happen! -transitions (Buf str) (In _) _ = Buf str -- Dummy response - -- error "This shouldn't happen: input transition with full buffer" + where + mTransitions :: Model r -> Action r -> Response r -> Model r + mTransitions Empty (In str) _ = Buf str + mTransitions (Buf _) Echo _ = Empty + mTransitions Empty Echo _ = Empty + -- TODO: qcsm will match the case below. However we don't expect this to happen! + mTransitions (Buf str) (In _) _ = Buf str -- Dummy response + -- error "This shouldn't happen: input transition with full buffer" --- | There are no preconditions for this model. -preconditions :: Model Symbolic -> Action Symbolic -> Logic -preconditions _ _ = Top + -- | There are no preconditions for this model. + mPreconditions :: Model Symbolic -> Action Symbolic -> Logic + mPreconditions _ _ = Top --- | Post conditions for the system. -postconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic -postconditions Empty (In _) InAck = Top -postconditions (Buf _) (In _) ErrFull = Top -postconditions _ (In _) _ = Bot -postconditions Empty Echo ErrEmpty = Top -postconditions Empty Echo _ = Bot -postconditions (Buf str) Echo (Out out) = str .== out -postconditions (Buf _) Echo _ = Bot + -- | Post conditions for the system. + mPostconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic + mPostconditions Empty (In _) InAck = Top + mPostconditions (Buf _) (In _) ErrFull = Top + mPostconditions _ (In _) _ = Bot + mPostconditions Empty Echo ErrEmpty = Top + mPostconditions Empty Echo _ = Bot + mPostconditions (Buf str) Echo (Out out) = str .== out + mPostconditions (Buf _) Echo _ = Bot --- | Generator for symbolic actions. -generator :: Model Symbolic -> Maybe (Gen (Action Symbolic)) -generator _ = Just $ oneof - [ In <$> arbitrary - , return Echo - ] + -- | Generator for symbolic actions. + mGenerator :: Model Symbolic -> Maybe (Gen (Action Symbolic)) + mGenerator _ = Just $ oneof + [ In <$> arbitrary + , return Echo + ] --- | Trivial shrinker. -shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic] -shrinker _ _ = [] + -- | Trivial shrinker. + mShrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic] + mShrinker _ _ = [] --- | Here we'd do the dispatch to the actual SUT. -semantics :: Env -> Action Concrete -> IO (Response Concrete) -semantics env (In str) = do - success <- input env str - return $ if success - then InAck - else ErrFull -semantics env Echo = maybe ErrEmpty Out <$> output env + -- | Here we'd do the dispatch to the actual SUT. + mSemantics :: Action Concrete -> IO (Response Concrete) + mSemantics (In str) = do + success <- input env str + return $ if success + then InAck + else ErrFull + mSemantics Echo = maybe ErrEmpty Out <$> output env --- | What is the mock for? -mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic) -mock Empty (In _) = return InAck -mock (Buf _) (In _) = return ErrFull -mock Empty Echo = return ErrEmpty -mock (Buf str) Echo = return (Out str) + -- | What is the mock for? + mMock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic) + mMock Empty (In _) = return InAck + mMock (Buf _) (In _) = return ErrFull + mMock Empty Echo = return ErrEmpty + mMock (Buf str) Echo = return (Out str) deriving anyclass instance ToExpr (Model Concrete) diff --git a/test/MemoryReference.hs b/test/MemoryReference.hs --- a/test/MemoryReference.hs +++ b/test/MemoryReference.hs @@ -224,7 +224,7 @@ prop_parallel' :: Bug -> Property prop_parallel' bug = forAllParallelCommands sm' Nothing $ \cmds -> monadicIO $ do - prettyParallelCommands cmds =<< runParallelCommands' (pure sm') complete cmds + prettyParallelCommands cmds =<< runParallelCommands' sm' complete cmds where sm' = sm bug complete :: Command Concrete -> Response Concrete diff --git a/test/Mock.hs b/test/Mock.hs --- a/test/Mock.hs +++ b/test/Mock.hs @@ -24,7 +24,7 @@ import Prelude import Test.QuickCheck import Test.QuickCheck.Monadic - (monadicIO) + (monadicIO, run) import Test.StateMachine import Test.StateMachine.DotDrawing import Test.StateMachine.TreeDiff @@ -95,31 +95,31 @@ shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic] shrinker _ _ = [] -sm :: IO (StateMachine Model Command IO Response) -sm = do - counter <- newMVar 0 - pure $ StateMachine initModel transition precondition postcondition +sm :: MVar Int -> StateMachine Model Command IO Response +sm counter = StateMachine initModel transition precondition postcondition Nothing generator shrinker (semantics counter) mock noCleanup smUnused :: StateMachine Model Command IO Response -smUnused = StateMachine initModel transition precondition postcondition - Nothing generator shrinker e mock noCleanup +smUnused = sm e where e = error "SUT must not be used" prop_sequential_mock :: Property prop_sequential_mock = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do - (hist, _model, res) <- runCommandsWithSetup sm cmds + counter <- run $ newMVar 0 + (hist, _model, res) <- runCommands (sm counter) cmds prettyCommands smUnused hist (res === Ok) prop_parallel_mock :: Property prop_parallel_mock = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do - ret <- runParallelCommandsWithSetup sm cmds + counter <- run $ newMVar 0 + ret <- runParallelCommands (sm counter) cmds prettyParallelCommandsWithOpts cmds opts ret where opts = Just $ GraphOptions "mock-test-output.png" Png prop_nparallel_mock :: Property prop_nparallel_mock = forAllNParallelCommands smUnused 3 $ \cmds -> monadicIO $ do - ret <- runNParallelCommandsWithSetup sm cmds + counter <- run $ newMVar 0 + ret <- runNParallelCommands (sm counter) cmds prettyNParallelCommandsWithOpts cmds opts ret where opts = Just $ GraphOptions "mock-np-test-output.png" Png diff --git a/test/SQLite.hs b/test/SQLite.hs --- a/test/SQLite.hs +++ b/test/SQLite.hs @@ -51,6 +51,7 @@ (Generic, Generic1) import Prelude import System.Directory +import System.FilePath import Test.QuickCheck import Test.QuickCheck.Monadic import Test.StateMachine @@ -279,16 +280,8 @@ deriving anyclass instance ToExpr DBModel deriving anyclass instance ToExpr (Model Concrete) -sm :: MonadUnliftIO m => String -> m (StateMachine Model (At Cmd) m (At Resp)) -sm folder = do - liftIO $ removePathForcibly folder - liftIO $ createDirectory folder - poolBackend <- runNoLoggingT $ createSqliteAsyncPool (pack folder <> "/persons.db") 5 - _ <- flip runSqlAsyncWrite poolBackend $ do - _ <- runMigrationQuiet $ migrate entityDefs $ entityDef (Nothing :: Maybe Person) - runMigrationQuiet $ migrate entityDefs $ entityDef (Nothing :: Maybe Car) - lock <- liftIO $ newMVar () - pure $ StateMachine { +sm :: MonadIO m => String -> AsyncWithPool SqlBackend -> MVar () -> StateMachine Model (At Cmd) m (At Resp) +sm folder poolBackend lock = StateMachine { initModel = initModelImpl , transition = transitionImpl , precondition = preconditionImpl @@ -304,21 +297,9 @@ } smUnused :: StateMachine Model (At Cmd) IO (At Resp) -smUnused = - StateMachine { - initModel = initModelImpl - , transition = transitionImpl - , precondition = preconditionImpl - , postcondition = postconditionImpl - , invariant = Nothing - , generator = generatorImpl - , shrinker = shrinkerImpl - , semantics = e - , mock = mockImpl - , cleanup = e - } - where - e = error "SUT must not be used" +smUnused = sm e e e + where + e = error "SUT must not be used" generatorImpl :: Model Symbolic -> Maybe (Gen (At Cmd Symbolic)) generatorImpl _model = Just $ At <$> @@ -350,16 +331,29 @@ clean :: MonadIO m => String -> Model Concrete -> m () clean folder _ = liftIO $ removePathForcibly folder +mkEnv :: FilePath -> IO (AsyncWithPool SqlBackend, MVar ()) +mkEnv name = do + removePathForcibly name + createDirectory name + db <- runNoLoggingT $ createSqliteAsyncPool (pack $ name "persons.db") 5 + _ <- flip runSqlAsyncWrite db $ do + _ <- runMigrationQuiet $ migrate entityDefs $ entityDef (Nothing :: Maybe Person) + runMigrationQuiet $ migrate entityDefs $ entityDef (Nothing :: Maybe Car) + lock <- newMVar () + pure (db, lock) + prop_sequential_sqlite :: Property prop_sequential_sqlite = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do - (hist, _model, res) <- runCommandsWithSetup (sm "sqlite-seq") cmds + (db, lock) <- run $ mkEnv "sqlite-seq" + (hist, _model, res) <- runCommands (sm "sqlite-seq" db lock) cmds prettyCommands smUnused hist $ res === Ok prop_parallel_sqlite :: Property prop_parallel_sqlite = - forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do - ret <- runParallelCommandsNTimesWithSetup 1 (sm "sqlite-par") cmds + forAllParallelCommandsNTimes smUnused Nothing 1 $ \cmds -> monadicIO $ do + (db, lock) <- run $ mkEnv "sqlite-par" + ret <- runParallelCommands (sm "sqlite-par" db lock) cmds prettyParallelCommandsWithOpts cmds (Just $ GraphOptions "sqlite.jpeg" Jpeg) ret instance Bifoldable t => Rank2.Foldable (At t) where diff --git a/test/Schema.hs b/test/Schema.hs --- a/test/Schema.hs +++ b/test/Schema.hs @@ -1,19 +1,19 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE QuasiQuotes #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module Schema ( Person (..) diff --git a/test/ShrinkingProps.hs b/test/ShrinkingProps.hs --- a/test/ShrinkingProps.hs +++ b/test/ShrinkingProps.hs @@ -319,7 +319,7 @@ precondition :: Model Symbolic -> Cmd :@ Symbolic -> Logic precondition (Model _ knownRefs _) (At cmd) = - forall (toList cmd) (`member` map fst knownRefs) + forAll (toList cmd) (`member` map fst knownRefs) postcondition :: HasCallStack => Model Concrete -> Cmd :@ Concrete -> Resp :@ Concrete -> Logic @@ -705,10 +705,9 @@ cmdsChucks = chunksOf n' sx sfxs = (\c -> [c]) . QSM.Commands <$> cmdsChucks nParallelCmd = QSM.ParallelCommands {prefix = QSM.Commands px, suffixes = sfxs} - res <- runNParallelCommandsNTimes 1 sm nParallelCmd - let (hist', _ret) = unzip [ (a, c) | (a, _, c) <- res ] - let events = snd <$> (QSM.unHistory hist) - events' = snd <$> (concat (QSM.unHistory <$> hist')) + (hist', _, _ret) <- runNParallelCommands sm nParallelCmd + let events = snd <$> QSM.unHistory hist + events' = snd <$> QSM.unHistory hist' return $ cmpList equalH events' events {------------------------------------------------------------------------------- diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -19,10 +19,10 @@ import Test.Tasty.QuickCheck (expectFailure, testProperty, withMaxSuccess) -import Bookstore as Store +import Bookstore as Store import CircularBuffer import Cleanup -import qualified CrudWebserverDb as WS +import qualified CrudWebserverDb as WS import DieHard import Echo import ErrorEncountered @@ -37,8 +37,6 @@ import TicketDispenser import qualified UnionFind --- RQlite tests fail, see #14 - ------------------------------------------------------------------------ tests :: Bool -> TestTree @@ -107,15 +105,13 @@ $ expectFailure $ withMaxSuccess 1000 $ prop_parallel_clean (Eq True) Cleanup.NoBug NoOp , testProperty "3-threadsRegularNoOp" $ prop_nparallel_clean 3 Regular Cleanup.NoBug NoOp - , testProperty "3-threadsRegular" - $ expectFailure $ prop_nparallel_clean 3 Regular Cleanup.NoBug ReDo + , testProperty "3-threadsRegular" $ prop_nparallel_clean 3 Regular Cleanup.NoBug ReDo , testProperty "3-threadsRegularExc" $ expectFailure $ prop_nparallel_clean 3 Regular Cleanup.Exception NoOp , testProperty "3-threadsRegularExc" $ expectFailure $ prop_nparallel_clean 3 Regular Cleanup.Exception ReDo , testProperty "3-threadsFilesNoOp" $ prop_nparallel_clean 3 Files Cleanup.NoBug NoOp - , testProperty "3-threadsFiles" - $ expectFailure $ prop_nparallel_clean 3 Files Cleanup.NoBug ReDo + , testProperty "3-threadsFiles" $ prop_nparallel_clean 3 Files Cleanup.NoBug ReDo , testProperty "3-threadsFilesExcNoOp" $ prop_nparallel_clean 3 Files Cleanup.Exception NoOp , testProperty "3-threadsFilesExc" $ expectFailure $ withMaxSuccess 1000 $ prop_nparallel_clean 3 Files Cleanup.Exception ReDo @@ -127,13 +123,6 @@ , testGroup "SQLite" [ testProperty "Parallel" prop_parallel_sqlite ] - -- Rqlite tests fail, see #14 - --, testGroup "Rqlite" - -- [ whenDocker docker0 "rqlite" $ testProperty "parallel" $ withMaxSuccess 10 $ prop_parallel_rqlite (Just Weak) - -- we currently don't add other properties, because they interfere (Tasty runs tests on parallel) - -- , testProperty "sequential" $ withMaxSuccess 10 $ prop_sequential_rqlite (Just Weak) - -- , testProperty "sequential-stale" $ expectFailure $ prop_sequential_rqlite (Just RQlite.None) - -- ] , testGroup "ErrorEncountered" [ testProperty "Sequential" prop_error_sequential , testProperty "Parallel" prop_error_parallel diff --git a/test/TicketDispenser.hs b/test/TicketDispenser.hs --- a/test/TicketDispenser.hs +++ b/test/TicketDispenser.hs @@ -195,40 +195,39 @@ run lock liftIO $ cleanupLock lock -sm :: SharedExclusive -> IO (StateMachine Model Action IO Response) -sm se = do - lock <- setupLock - pure $ StateMachine initModel transitions preconditions postconditions - Nothing generator shrinker (semantics se lock) mock (const $ cleanupLock lock) +sm :: SharedExclusive -> DbLock -> StateMachine Model Action IO Response +sm se files = StateMachine + initModel transitions preconditions postconditions + Nothing generator shrinker (semantics se files) mock noCleanup -smUnused :: StateMachine Model Action IO Response -smUnused = - StateMachine initModel transitions preconditions postconditions - Nothing generator shrinker e mock noCleanup - where - e = error "SUT must not be used" +smUnused :: SharedExclusive -> StateMachine Model Action IO Response +smUnused se = sm se (error "dblock used during command creation") -- Sequentially the model is consistent (even though the lock is -- shared). prop_ticketDispenser :: Property prop_ticketDispenser = - forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do - (hist, _, res) <- runCommandsWithSetup (sm Shared) cmds - prettyCommands smUnused hist $ + forAllCommands (smUnused Shared) Nothing $ \cmds -> monadicIO $ + withDbLock $ \ioLock -> do + let sm' = sm Shared ioLock + (hist, _, res) <- runCommands sm' cmds + prettyCommands sm' hist $ checkCommandNames cmds (res === Ok) prop_ticketDispenserParallel :: SharedExclusive -> Property prop_ticketDispenserParallel se = - forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do - let sm' = sm se - prettyParallelCommands cmds =<< runParallelCommandsNTimesWithSetup 100 sm' cmds + forAllParallelCommandsNTimes (smUnused se) Nothing 100 $ \cmds -> monadicIO $ + withDbLock $ \ioLock -> do + let sm' = sm se ioLock + prettyParallelCommands cmds =<< runParallelCommands sm' cmds prop_ticketDispenserNParallel :: SharedExclusive -> Int -> Property prop_ticketDispenserNParallel se np = - forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do - let sm' = sm se - prettyNParallelCommands cmds =<< runNParallelCommandsWithSetup sm' cmds + forAllNParallelCommands (smUnused se) np $ \cmds -> monadicIO $ + withDbLock $ \ioLock -> do + let sm' = sm se ioLock + prettyNParallelCommands cmds =<< runNParallelCommands sm' cmds -- So long as the file locks are exclusive, i.e. not shared, the -- parallel property passes. diff --git a/tree-diff/Test/StateMachine/TreeDiff/Pretty.hs b/tree-diff/Test/StateMachine/TreeDiff/Pretty.hs --- a/tree-diff/Test/StateMachine/TreeDiff/Pretty.hs +++ b/tree-diff/Test/StateMachine/TreeDiff/Pretty.hs @@ -10,7 +10,7 @@ prettyExpr, prettyEditExpr, prettyEditExprCompact, - -- * ansi-wl-pprint + -- * prettyprinter ansiWlPretty, ansiWlExpr, ansiWlEditExpr, @@ -36,8 +36,9 @@ import qualified Data.Map as Map +import qualified Prettyprinter as PP +import qualified Prettyprinter.Render.Terminal as PP import qualified Text.PrettyPrint as HJ -import qualified Text.PrettyPrint.ANSI.Leijen as WL -- | Because we don't want to commit to single pretty printing library, -- we use explicit dictionary. @@ -102,8 +103,8 @@ headNotMP ('+' : _) = False headNotMP _ = True - isValidString s - | length s >= 2 && head s == '"' && last s == '"' = + isValidString s@('"':_:_) + | last s == '"' = case readMaybe s :: Maybe String of Just _ -> True Nothing -> False @@ -203,34 +204,34 @@ prettyEditExprCompact = ppEditExprCompact prettyPretty ------------------------------------------------------------------------------- --- ansi-wl-pprint +-- prettyprinter ------------------------------------------------------------------------------- --- | 'Pretty' via @ansi-wl-pprint@ library (with colors). -ansiWlPretty :: Pretty WL.Doc +-- | 'Pretty' via @prettyprinter@ library (with colors). +ansiWlPretty :: Pretty (PP.Doc PP.AnsiStyle) ansiWlPretty = Pretty - { ppCon = WL.text - , ppRec = WL.encloseSep WL.lbrace WL.rbrace WL.comma - . map (\(fn, d) -> WL.text fn WL.<+> WL.equals WL. d) - , ppLst = WL.list - , ppCpy = WL.dullwhite - , ppIns = \d -> WL.green $ WL.plain $ WL.char '+' WL.<> d - , ppDel = \d -> WL.red $ WL.plain $ WL.char '-' WL.<> d - , ppSep = WL.sep - , ppParens = WL.parens - , ppHang = \d1 d2 -> WL.hang 2 (d1 WL. d2) + { ppCon = PP.pretty + , ppRec = PP.encloseSep PP.lbrace PP.rbrace PP.comma + . map (\(fn, d) -> PP.pretty fn PP.<+> PP.equals <> PP.softline <> d) + , ppLst = PP.list + , ppCpy = PP.annotate (PP.colorDull PP.White) + , ppIns = \d -> PP.annotate (PP.color PP.Green) $ PP.unAnnotate $ PP.pretty '+' PP.<> d + , ppDel = \d -> PP.annotate (PP.color PP.Red) $ PP.unAnnotate $ PP.pretty '-' PP.<> d + , ppSep = PP.sep + , ppParens = PP.parens + , ppHang = \d1 d2 -> PP.hang 2 (d1 <> PP.softline <> d2) } --- | Pretty print 'Expr' using @ansi-wl-pprint@. -ansiWlExpr :: Expr -> WL.Doc +-- | Pretty print 'Expr' using @prettyprinter@. +ansiWlExpr :: Expr -> PP.Doc PP.AnsiStyle ansiWlExpr = ppExpr ansiWlPretty --- | Pretty print @'Edit' 'EditExpr'@ using @ansi-wl-pprint@. -ansiWlEditExpr :: Edit EditExpr -> WL.Doc +-- | Pretty print @'Edit' 'EditExpr'@ using @prettyprinter@. +ansiWlEditExpr :: Edit EditExpr -> PP.Doc PP.AnsiStyle ansiWlEditExpr = ppEditExpr ansiWlPretty -- | Compact 'ansiWlEditExpr' -ansiWlEditExprCompact :: Edit EditExpr -> WL.Doc +ansiWlEditExprCompact :: Edit EditExpr -> PP.Doc PP.AnsiStyle ansiWlEditExprCompact = ppEditExprCompact ansiWlPretty ------------------------------------------------------------------------------- @@ -238,20 +239,20 @@ ------------------------------------------------------------------------------- -- | Like 'ansiWlPretty' but color the background. -ansiWlBgPretty :: Pretty WL.Doc +ansiWlBgPretty :: Pretty (PP.Doc PP.AnsiStyle) ansiWlBgPretty = ansiWlPretty - { ppIns = \d -> WL.ondullgreen $ WL.white $ WL.plain $ WL.char '+' WL.<> d - , ppDel = \d -> WL.ondullred $ WL.white $ WL.plain $ WL.char '-' WL.<> d + { ppIns = \d -> PP.annotate (PP.bgColorDull PP.Green <> PP.color PP.White) $ PP.unAnnotate $ PP.pretty '+' PP.<> d + , ppDel = \d -> PP.annotate (PP.bgColorDull PP.Red <> PP.color PP.White) $ PP.unAnnotate $ PP.pretty '-' PP.<> d } --- | Pretty print 'Expr' using @ansi-wl-pprint@. -ansiWlBgExpr :: Expr -> WL.Doc +-- | Pretty print 'Expr' using @prettyprinter@. +ansiWlBgExpr :: Expr -> PP.Doc PP.AnsiStyle ansiWlBgExpr = ppExpr ansiWlBgPretty --- | Pretty print @'Edit' 'EditExpr'@ using @ansi-wl-pprint@. -ansiWlBgEditExpr :: Edit EditExpr -> WL.Doc +-- | Pretty print @'Edit' 'EditExpr'@ using @prettyprinter@. +ansiWlBgEditExpr :: Edit EditExpr -> PP.Doc PP.AnsiStyle ansiWlBgEditExpr = ppEditExpr ansiWlBgPretty -- | Compact 'ansiWlBgEditExpr'. -ansiWlBgEditExprCompact :: Edit EditExpr -> WL.Doc +ansiWlBgEditExprCompact :: Edit EditExpr -> PP.Doc PP.AnsiStyle ansiWlBgEditExprCompact = ppEditExprCompact ansiWlBgPretty