quickcheck-state-machine 0.9.0 → 0.10.0
raw patch · 23 files changed
+521/−710 lines, 23 filesdep +prettyprinterdep +prettyprinter-ansi-terminaldep −ansi-wl-pprint
Dependencies added: prettyprinter, prettyprinter-ansi-terminal
Dependencies removed: ansi-wl-pprint
Files
- CHANGELOG.md +16/−0
- README.md +7/−117
- quickcheck-state-machine.cabal +18/−11
- src/Test/StateMachine.hs +3/−9
- src/Test/StateMachine/BoxDrawer.hs +4/−4
- src/Test/StateMachine/ConstructorName.hs +3/−3
- src/Test/StateMachine/Diffing.hs +5/−4
- src/Test/StateMachine/Logic.hs +5/−5
- src/Test/StateMachine/Parallel.hs +161/−231
- src/Test/StateMachine/Sequential.hs +58/−65
- src/Test/StateMachine/Types/Rank2.hs +3/−2
- src/Test/StateMachine/Utils.hs +2/−1
- test/Cleanup.hs +62/−58
- test/CrudWebserverDb.hs +2/−2
- test/Echo.hs +65/−73
- test/MemoryReference.hs +1/−1
- test/Mock.hs +10/−10
- test/SQLite.hs +22/−28
- test/Schema.hs +16/−16
- test/ShrinkingProps.hs +4/−5
- test/Spec.hs +4/−15
- test/TicketDispenser.hs +19/−20
- tree-diff/Test/StateMachine/TreeDiff/Pretty.hs +31/−30
CHANGELOG.md view
@@ -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
README.md view
@@ -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
quickcheck-state-machine.cabal view
@@ -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 <https://github.com/stevana/quickcheck-state-machine#readme>@@ -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
src/Test/StateMachine.hs view
@@ -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
src/Test/StateMachine/BoxDrawer.hs view
@@ -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
src/Test/StateMachine/ConstructorName.hs view
@@ -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
src/Test/StateMachine/Diffing.hs view
@@ -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)
src/Test/StateMachine/Logic.hs view
@@ -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
src/Test/StateMachine/Parallel.hs view
@@ -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 ]
src/Test/StateMachine/Sequential.hs view
@@ -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."
src/Test/StateMachine/Types/Rank2.hs view
@@ -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(..), (<$>))
src/Test/StateMachine/Utils.hs view
@@ -41,7 +41,8 @@ import Prelude -import Data.Bifunctor (second)+import Data.Bifunctor+ (second) import Data.List (foldl') import Test.QuickCheck
test/Cleanup.hs view
@@ -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`
test/CrudWebserverDb.hs view
@@ -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
test/Echo.hs view
@@ -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)
test/MemoryReference.hs view
@@ -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
test/Mock.hs view
@@ -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
test/SQLite.hs view
@@ -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
test/Schema.hs view
@@ -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 (..)
test/ShrinkingProps.hs view
@@ -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 {-------------------------------------------------------------------------------
test/Spec.hs view
@@ -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
test/TicketDispenser.hs view
@@ -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.
tree-diff/Test/StateMachine/TreeDiff/Pretty.hs view
@@ -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