quickcheck-state-machine 0.7.1 → 0.7.2
raw patch · 22 files changed
+919/−425 lines, 22 filesdep −HTTPdep ~persistentdep ~persistent-sqlitedep ~persistent-template
Dependencies removed: HTTP
Dependency ranges changed: persistent, persistent-sqlite, persistent-template, time
Files
- CHANGELOG.md +10/−0
- LICENSE +4/−3
- README.md +186/−20
- quickcheck-state-machine.cabal +12/−8
- src/Test/StateMachine.hs +5/−0
- src/Test/StateMachine/Lockstep/Auxiliary.hs +1/−1
- src/Test/StateMachine/Lockstep/NAry.hs +164/−30
- src/Test/StateMachine/Lockstep/Simple.hs +70/−9
- src/Test/StateMachine/Parallel.hs +177/−90
- src/Test/StateMachine/Sequential.hs +29/−21
- src/Test/StateMachine/Types.hs +1/−1
- test/Cleanup.hs +57/−56
- test/Echo.hs +78/−74
- test/IORefs.hs +20/−0
- test/MemoryReference.hs +1/−1
- test/Mock.hs +11/−11
- test/ProcessRegistry.hs +1/−1
- test/RQlite.hs +28/−38
- test/SQLite.hs +32/−27
- test/ShrinkingProps.hs +1/−1
- test/Spec.hs +11/−14
- test/TicketDispenser.hs +20/−19
CHANGELOG.md view
@@ -1,3 +1,13 @@+#### 0.7.2 (2023-4-20)++ * Fix compatibility with GHC 9.0 and 9.2 (PR #7, thanks @edsko);++ * Various documentation improvements (PR #9, #10 and #13, thanks @Jasagredo);++ * Introduce new `runXCommandsXWithSetup` which allow for monadic+ initialization of the state machine for each test case execution (PR #12,+ thanks @Jasagredo).+ #### 0.7.1 (2021-8-17) * Update links and references from the old archived repo at the
LICENSE view
@@ -1,6 +1,7 @@-Copyright (c) 2017-2020 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley,- Xia Li-yao, Robert Danitz, Thomas Winant, Edsko de Vries,- Momoko Hattori, Kostas Dermentzis, Adam Boniecki+Copyright (c) 2017-2023 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley,+ Xia Li-yao, Robert Danitz, Thomas Winant, Edsko de+ Vries, Momoko Hattori, Kostas Dermentzis, Adam Boniecki,+ Javier Sagredo All rights reserved.
README.md view
@@ -108,7 +108,8 @@ The transition function explains how actions change the model. Note that the transition function is polymorphic in `r`. The reason for this is that we use-the transition function both while generating and executing.+the transition function while generating and shrinking (with `r ~ Symbolic`) and+when executing (with `r ~ Concrete`) sequences of commands. ```haskell transition :: Eq1 r => Model r -> Command r -> Response r -> Model r@@ -123,8 +124,8 @@ update ref i m = (ref, i) : filter ((/= ref) . fst) m ``` -Post-conditions are checked after we executed an action and got access to the-result.+Post-conditions are checked after we executed an action and got a response from+the implementation (via `semantics`). ```haskell postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic@@ -168,18 +169,35 @@ Increment _ -> pure Incremented ``` -(`mock` is a hack to make it possible for responses to have multiple reference,-and an experiment which maybe one day will let us create mocked APIs. See issue-[#236](https://github.com/advancedtelematic/quickcheck-state-machine/issues/236)-for further details.)+> `mock` is a hack to make it possible for responses to have multiple reference,+> and an experiment which maybe one day will let us create mocked APIs. See issue+> [#236](https://github.com/advancedtelematic/quickcheck-state-machine/issues/236)+> for further details. +Despite what is mentioned in the quoted issue, the `mock` function *will* be used+when advancing the model in the `Symbolic` layer, in particular in two places:++- when generating commands the model is advanced with a command generated by the+ model itself and the mocked response to that command (see+ `generateCommandsState`);++- when shrinking the list of commands by mocking responses to those commands+ which are used to advance the model and then preconditions for the shrinked+ commands are checked on that advanced model (see `shrinkAndValidate`).++Therefore, `mock` *must* provide responses that will make the model advance *on+par* with the implementation. Note that as responses might define fields which+are expected to be used only by `postcondition`, those might be filled with+dummy values in `mock` as the `postcondition` is called only with the `Concrete`+response from the implementation.+ To be able to fit the code on a line we pack up all of them above into a record. ```haskell sm :: Bug -> StateMachine Model Command IO Response sm bug = StateMachine initModel transition precondition postcondition- Nothing generator shrinker (semantics bug) mock+ Nothing generator shrinker (semantics bug) mock noCleanup ``` We can now define a sequential property as follows.@@ -240,7 +258,7 @@ ```haskell prop_parallel :: Bug -> Property-prop_parallel bug = forAllParallelCommands sm' $ \cmds -> monadicIO $ do+prop_parallel bug = forAllParallelCommands sm' Nothing $ \cmds -> monadicIO $ do prettyParallelCommands cmds =<< runParallelCommands sm' cmds where sm' = sm bug@@ -345,24 +363,157 @@ race conditions -- which normally can be tricky to test for. It works as follows: - 1. generate a list of actions that will act as a sequential prefix for the- parallel program (think of this as an initialisation bit that setups up- some state);+ 1. generate a list of actions and split it in two (or more) parts: - 2. generate two lists of actions that will act as parallel suffixes;+ - a first part that will be run sequentially, called the _prefix_ (think+ of this as an initialisation bit that setups up some state);+ - a second part (the _suffix_) that will be split in sublists which will+ be run in parallel (see `parallelSafe` to understand how it determines+ that a sequence of commands can be run in parallel). More than one+ suffix can be generated, i.e. this second step can be done multiple+ times with the part of the generated list that doesn't belong to the+ prefix. - 3. execute the prefix sequentially;+ 2. initialize the state machine if necessary (see [this](#sut-initialization)); - 4. execute the suffixes in parallel and gather the a trace (or history) of- invocations and responses of each action;+ 3. execute the prefix sequentially as in the section above (checking pre- and+ post-conditions); - 5. try to find a possible sequential interleaving of action invocations and- responses that respects the post-conditions.+ 4. execute the suffixes in parallel without checking pre/post-conditions+ and gather the trace (or history) of invocations and responses of each+ action; -The last step basically tries to find+```+ ┌── no checks aside from ensuring no exception was thrown+ │+ ╭─────────┴──────────╮++ ┌─ [C] ──┐ ┌ [F, G] ┐ ◀─╮+Commands: [A, B] ─┤ ├──┤ │ ├─ executed `concurrently`+ └ [D, E] ┘ └ [H, I] ┘ ◀─╯++ ╰─┬──╯ ▲ ▲+ │ ╰─────┬────╯+ │ └── groups are not run in parallel+ │ i.e [C, D, E] will run (and+ │ finish) before F or H are+ │ started+ │+ └── pre/postconditions and invariant checked+ executed sequentially+```++ 5. 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+ 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+ 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+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+evaluating possible interleavings. This particularly means that the model must+be correct with respect to sequential execution before used in parallel testing.++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+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.++#### 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 Here are some more examples to get you started:@@ -469,7 +620,7 @@ * IOHK are using a state machine models in several [places](https://github.com/search?l=Haskell&q=org%3Ainput-output-hk+Test.StateMachine&type=Code). For example- [here](https://github.com/input-output-hk/ouroboros-network/blob/master/ouroboros-consensus/test-storage/Test/Ouroboros/Storage/FS/StateMachine.hs)+ [here](https://github.com/input-output-hk/ouroboros-network/blob/master/ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/FS/StateMachine.hs) is a test of a mock file system that they in turn use to simulate file system errors when testing a blockchain database. The following blog [post](http://www.well-typed.com/blog/2019/01/qsm-in-depth/) describes their@@ -604,6 +755,21 @@ based [testing](https://hypothesis.readthedocs.io/en/latest/stateful.html) (no parallel property).++### History and current status++This library was originally developed while I was working at *ATS Advanced+Telematic Systems GmbH* between 2017 and 2018. In 2018 *HERE Europe B.V*+acquired *ATS* and took over control over the+[advancedtelematic](https://github.com/advancedtelematic) GitHub organisation. I+left *HERE* in 2019 and in 2021 they archived the old+[`quickcheck-state-machine`](https://github.com/advancedtelematic/quickcheck-state-machine)+repo making it read-only -- that's when this fork was created.++I no longer use `quickcheck-state-machine` on a daily basis, and have no plans+for making any major changes. That said, I consider the library fairly feature+complete and stable and I'm happy to do minor maintenance work. I'm also happy+to help and mentor anyone willing to take on a more active development role. ### License
quickcheck-state-machine.cabal view
@@ -1,5 +1,5 @@ name: quickcheck-state-machine-version: 0.7.1+version: 0.7.2 synopsis: Test monadic programs using state machine based models description: See README at <https://github.com/stevana/quickcheck-state-machine#readme> homepage: https://github.com/stevana/quickcheck-state-machine#readme@@ -9,14 +9,14 @@ maintainer: Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk> copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH; 2018-2019, HERE Europe B.V.;- 2019-2021, Stevan Andjelkovic.+ 2019-2023, Stevan Andjelkovic. category: Testing build-type: Simple extra-source-files: README.md , CHANGELOG.md , CONTRIBUTING.md cabal-version: >=1.10-tested-with: GHC == 8.4.3, GHC == 8.6.5, GHC == 8.8.3+tested-with: GHC == 8.4.3, GHC == 8.6.5, GHC == 8.8.3, GHC == 8.10.7 library hs-source-dirs: src@@ -30,6 +30,8 @@ -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction+ -Wno-prepositive-qualified-module+ -Wno-missing-safe-haskell-mode exposed-modules: Test.StateMachine , Test.StateMachine.BoxDrawer , Test.StateMachine.ConstructorName@@ -93,15 +95,16 @@ hashable, hashtables, hs-rqlite >= 0.1.2.0,- HTTP, http-client, monad-logger, mtl, network,- persistent >= 2.10.3,+ -- if we want to use later versions of persistent, we+ -- need to make some minor changes to the test suite:+ persistent >= 2.10.4 && < 2.11, persistent-postgresql,- persistent-sqlite,- persistent-template,+ persistent-sqlite < 2.11,+ persistent-template < 2.11, postgresql-simple, pretty-show, process,@@ -123,7 +126,6 @@ tasty-quickcheck, text, tree-diff,- time, vector >=0.12.0.1, wai, warp,@@ -162,6 +164,8 @@ -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction+ -Wno-prepositive-qualified-module+ -Wno-missing-safe-haskell-mode default-language: Haskell2010 source-repository head
src/Test/StateMachine.hs view
@@ -19,6 +19,7 @@ forAllCommands , existsCommands , runCommands+ , runCommandsWithSetup , prettyCommands , prettyCommands' , checkCommandNames@@ -35,12 +36,16 @@ , forAllParallelCommands , forAllNParallelCommands , runNParallelCommands+ , runNParallelCommandsWithSetup , runParallelCommands+ , runParallelCommandsWithSetup , runParallelCommands' , runParallelCommandsNTimes+ , runParallelCommandsNTimesWithSetup , runNParallelCommandsNTimes' , runParallelCommandsNTimes' , runNParallelCommandsNTimes+ , runNParallelCommandsNTimesWithSetup , prettyNParallelCommands , prettyParallelCommands , prettyParallelCommandsWithOpts
src/Test/StateMachine/Lockstep/Auxiliary.hs view
@@ -61,7 +61,7 @@ ntraverse :: (NTraversable f, Applicative m, SListI xs) => (forall a. Elem xs a -> g a -> m (h a)) -> f g xs -> m (f h xs)-ntraverse = nctraverse (Proxy @Top)+ntraverse f = nctraverse (Proxy @Top) f ncfmap :: (NTraversable f, All c xs) => proxy c
src/Test/StateMachine/Lockstep/NAry.hs view
@@ -24,10 +24,12 @@ , Resp , RealHandles , MockHandle- , RealMonad , Test+ , Tag -- * Test term-level parameters , StateMachineTest(..)+ , Event(..)+ , hoistStateMachineTest -- * Handle instantiation , At(..) , (:@)@@ -39,6 +41,9 @@ -- * Running the tests , prop_sequential , prop_parallel+ -- * Examples+ , showLabelledExamples'+ , showLabelledExamples -- * Translate to state machine model , toStateMachine ) where@@ -58,9 +63,12 @@ import Test.QuickCheck import Test.QuickCheck.Monadic import Test.StateMachine+ hiding (showLabelledExamples, showLabelledExamples') import qualified Data.Monoid as M import qualified Data.TreeDiff as TD+import qualified Test.StateMachine.Labelling as Label+import qualified Test.StateMachine.Sequential as Seq import qualified Test.StateMachine.Types as QSM import qualified Test.StateMachine.Types.Rank2 as Rank2 @@ -70,13 +78,50 @@ Test type-level parameters -------------------------------------------------------------------------------} -type family MockState t :: Type-data family Cmd t :: (Type -> Type) -> [Type] -> Type-data family Resp t :: (Type -> Type) -> [Type] -> Type-type family RealHandles t :: [Type]-data family MockHandle t a :: Type-type family RealMonad t :: Type -> Type+-- | Mock state+--+-- The @t@ argument (here and elsewhere) is a type-level tag that combines all+-- aspects of the test; it does not need any term-level constructors+--+-- > data MyTest+-- > type instance MockState MyTest = ..+type family MockState t :: Type +-- | Type-level list of the types of the handles in the system under test+--+-- NOTE: If your system under test only requires a single real handle, you+-- might consider using "Test.StateMachine.Lockstep.Simple" instead.+type family RealHandles t :: [Type]++-- | Mock handles+--+-- For each real handle @a@, @MockHandle t a@ is the corresponding mock handle.+data family MockHandle t a :: Type++-- | Commands+--+-- In @Cmd t f hs@, @hs@ is the list of real handle types, and @f@ is some+-- functor applied to each of them. Two typical instantiations are+--+-- > Cmd t I (RealHandles t) -- for the system under test+-- > Cmd t (MockHandle t) (RealHandles t) -- for the mock+data family Cmd t :: (Type -> Type) -> [Type] -> Type++-- | Responses+--+-- The type arguments are similar to those of @Cmd@. Two typical instances:+--+-- > Resp t I (RealHandles t) -- for the system under test+-- > Resp t (MockHandle t) (RealHandles t) -- for the mock+data family Resp t :: (Type -> Type) -> [Type] -> Type++-- | Tags+--+-- Tags are used when labelling execution runs in 'prop_sequential', as well as+-- when looking for minimal examples with a given label+-- ('showLabelledExamples').+type family Tag t :: Type+ {------------------------------------------------------------------------------- Reference environments -------------------------------------------------------------------------------}@@ -164,15 +209,19 @@ , All (And ToExpr (Compose ToExpr (MockHandle t))) (RealHandles t) ) => ToExpr (Model t Concrete) -initModel :: StateMachineTest t -> Model t r+initModel :: StateMachineTest t m -> Model t r initModel StateMachineTest{..} = Model initMock (Refss (hpure (Refs []))) {------------------------------------------------------------------------------- High level API -------------------------------------------------------------------------------} -data StateMachineTest t =- ( Monad (RealMonad t)+-- | State machine test+--+-- This captures the design patterns sketched in+-- <https://well-typed.com/blog/2019/01/qsm-in-depth/>.+data StateMachineTest t m =+ ( Monad m -- Requirements on the handles , All Typeable (RealHandles t) , All Eq (RealHandles t)@@ -191,19 +240,37 @@ -- MockState , Show (MockState t) , ToExpr (MockState t)+ -- Tags+ , Show (Tag t) ) => StateMachineTest { runMock :: Cmd t (MockHandle t) (RealHandles t) -> MockState t -> (Resp t (MockHandle t) (RealHandles t), MockState t)- , runReal :: Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))+ , runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t)) , initMock :: MockState t , newHandles :: forall f. Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t) , generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic)) , shrinker :: Model t Symbolic -> Cmd t :@ Symbolic -> [Cmd t :@ Symbolic]- , cleanup :: Model t Concrete -> RealMonad t ()+ , cleanup :: Model t Concrete -> m ()+ , tag :: [Event t Symbolic] -> [Tag t] } -semantics :: StateMachineTest t+hoistStateMachineTest :: Monad n+ => (forall a. m a -> n a)+ -> StateMachineTest t m+ -> StateMachineTest t n+hoistStateMachineTest f StateMachineTest {..} = StateMachineTest {+ runMock = runMock+ , runReal = f . runReal+ , initMock = initMock+ , newHandles = newHandles+ , generator = generator+ , shrinker = shrinker+ , cleanup = f . cleanup+ , tag = tag+ }++semantics :: StateMachineTest t m -> Cmd t :@ Concrete- -> RealMonad t (Resp t :@ Concrete)+ -> m (Resp t :@ Concrete) semantics StateMachineTest{..} (At c) = (At . ncfmap (Proxy @Typeable) (const wrapConcrete)) <$> runReal (nfmap (const unwrapConcrete) c)@@ -234,7 +301,7 @@ find refss ix r = unRefs (npAt refss ix) ! r step :: Eq1 r- => StateMachineTest t+ => StateMachineTest t m -> Model t r -> Cmd t :@ r -> (Resp t (MockHandle t) (RealHandles t), MockState t)@@ -248,8 +315,8 @@ , mockResp :: Resp t (MockHandle t) (RealHandles t) } -lockstep :: forall t r. Eq1 r- => StateMachineTest t+lockstep :: forall t m r. Eq1 r+ => StateMachineTest t m -> Model t r -> Cmd t :@ r -> Resp t :@ r@@ -267,14 +334,14 @@ rss' = zipHandles (newHandles resp) (newHandles resp') transition :: Eq1 r- => StateMachineTest t+ => StateMachineTest t m -> Model t r -> Cmd t :@ r -> Resp t :@ r -> Model t r transition sm m c = after . lockstep sm m c -postcondition :: StateMachineTest t+postcondition :: StateMachineTest t m -> Model t Concrete -> Cmd t :@ Concrete -> Resp t :@ Concrete@@ -284,7 +351,7 @@ where e = lockstep sm m c r -symbolicResp :: StateMachineTest t+symbolicResp :: StateMachineTest t m -> Model t Symbolic -> Cmd t :@ Symbolic -> GenSym (Resp t :@ Symbolic)@@ -307,8 +374,8 @@ sameRef :: Reference a Symbolic -> Reference a Symbolic -> Bool sameRef (QSM.Reference (QSM.Symbolic v)) (QSM.Reference (QSM.Symbolic v')) = v == v' -toStateMachine :: StateMachineTest t- -> StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))+toStateMachine :: StateMachineTest t m+ -> StateMachine (Model t) (At (Cmd t)) m (At (Resp t)) toStateMachine sm@StateMachineTest{} = StateMachine { initModel = initModel sm , transition = transition sm@@ -322,30 +389,97 @@ , invariant = Nothing } -prop_sequential :: RealMonad t ~ IO- => StateMachineTest t+-- | Sequential test+prop_sequential :: forall t.+ StateMachineTest t IO -> Maybe Int -- ^ (Optional) minimum number of commands -> Property-prop_sequential sm@StateMachineTest{} mMinSize =+prop_sequential sm@StateMachineTest{..} mMinSize = forAllCommands sm' mMinSize $ \cmds -> monadicIO $ do (hist, _model, res) <- runCommands sm' cmds prettyCommands sm' hist+ $ tabulate "Tags" (map show $ tagCmds cmds) $ res === Ok where sm' = toStateMachine sm -prop_parallel :: RealMonad t ~ IO- => StateMachineTest t+ tagCmds :: QSM.Commands (At (Cmd t)) (At (Resp t)) -> [Tag t]+ tagCmds = tag . map (fromLabelEvent sm) . Label.execCmds sm'++-- | Parallel test+--+-- NOTE: This currently does not do labelling.+prop_parallel :: StateMachineTest t IO -> Maybe Int -- ^ (Optional) minimum number of commands -> Property prop_parallel sm@StateMachineTest{} mMinSize = forAllParallelCommands sm' mMinSize $ \cmds ->- monadicIO $- prettyParallelCommands cmds- =<< runParallelCommands sm' cmds+ monadicIO $ do+ hist <- runParallelCommands sm' cmds+ -- TODO: Ideally we would tag here as well, but unlike 'prettyCommands',+ -- 'prettyParallelCommands' does not give us a hook to specify a+ -- 'Property', so this would require a change to the QSM core.+ prettyParallelCommands cmds hist where sm' = toStateMachine sm++{-------------------------------------------------------------------------------+ Labelling+-------------------------------------------------------------------------------}++-- | Translate QSM's 'Label.Event' into our 'Event'+--+-- The QSM 'Label.Event' is purely in terms of symbolic references. In order to+-- construct our 'Event' from this, we need to reconstruct the mock response.+-- We can do this, because we maintain a mapping between references and mock+-- handles in the model, irrespective of whether those references are symbolic+-- (as here) or concrete (during test execution). We can therefore apply this+-- mapping, and re-compute the mock response.+--+-- We could use 'lockstep' instead of 'step', but this would recompute the+-- new state, which is not necessary.+--+-- NOTE: This forgets the symbolic response in favour of the mock response.+-- This seems more in line with what we do elsewhere in the lockstep+-- infrastructure, but we could conceivably return both.+fromLabelEvent :: StateMachineTest t m+ -> Label.Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic+ -> Event t Symbolic+fromLabelEvent sm Label.Event{..} = Event{+ before = eventBefore+ , cmd = eventCmd+ , after = eventAfter+ , mockResp = resp'+ }+ where+ (resp', _st') = step sm eventBefore eventCmd++-- | Show minimal examples for each of the generated tags.+--+-- This is the analogue of 'Test.StateMachine.showLabelledExamples''.+-- See also 'showLabelledExamples'.+showLabelledExamples' :: StateMachineTest t m+ -> Maybe Int+ -- ^ Seed+ -> Int+ -- ^ Number of tests to run to find examples+ -> (Tag t -> Bool)+ -- ^ Tag filter (can be @const True@)+ -> IO ()+showLabelledExamples' sm@StateMachineTest{..} mReplay numTests =+ Seq.showLabelledExamples'+ (toStateMachine sm)+ mReplay+ numTests+ (tag . map (fromLabelEvent sm))++-- | Simplified form of 'showLabelledExamples''+showLabelledExamples :: StateMachineTest t m -> IO ()+showLabelledExamples sm@StateMachineTest{..} =+ Seq.showLabelledExamples+ (toStateMachine sm)+ (tag . map (fromLabelEvent sm)) {------------------------------------------------------------------------------- Rank2 instances
src/Test/StateMachine/Lockstep/Simple.hs view
@@ -20,8 +20,10 @@ , RealHandle , MockHandle , Test+ , Tag -- * Test term-level parameters , StateMachineTest(..)+ , Event(..) -- * Handle instantiation , At(..) , (:@)@@ -45,7 +47,7 @@ import Test.StateMachine import Test.StateMachine.Lockstep.Auxiliary import Test.StateMachine.Lockstep.NAry- (MockState)+ (MockState, Tag) import qualified Test.StateMachine.Lockstep.NAry as NAry @@ -53,11 +55,37 @@ Top-level parameters -------------------------------------------------------------------------------} -data family Cmd t :: Type -> Type-data family Resp t :: Type -> Type+-- | The type of the real handle in the system under test+--+-- The key difference between the " simple " lockstep infrastructure and the+-- n-ary lockstep infrastructure is that the former only supports a single+-- real handle, whereas the latter supports an arbitrary list of them. data family RealHandle t :: Type++-- | The type of the mock handle+--+-- NOTE: In the n-ary infrastructure, 'MockHandle' is a type family of /two/+-- arguments, because we have a mock handle for each real handle. Here, however,+-- we only /have/ a single real handle, so the " corresponding " real handle+-- is implicitly @RealHandle t@. data family MockHandle t :: Type +-- | Commands+--+-- In @Cmd t h@, @h@ is the type of the handle+--+-- > Cmd t (RealHandle t) -- for the system under test+-- > Cmd t (MockHandle t) -- for the mock+data family Cmd t :: Type -> Type++-- | Responses+--+-- In @Resp t h@, @h@ is the type of the handle+--+-- > Resp t (RealHandle t) -- for the system under test+-- > Resp t (MockHandle t) -- for the mock+data family Resp t :: Type -> Type+ {------------------------------------------------------------------------------- Default handle instantiation -------------------------------------------------------------------------------}@@ -87,15 +115,33 @@ } {-------------------------------------------------------------------------------+ Simplified event+-------------------------------------------------------------------------------}++data Event t r = Event {+ before :: Model t r+ , cmd :: Cmd t :@ r+ , after :: Model t r+ , mockResp :: Resp t (MockHandle t)+ }++eventToSimple :: (Functor (Cmd t), Functor (Resp t))+ => NAry.Event (Simple t) r -> Event t r+eventToSimple NAry.Event{..} = Event{+ before = modelToSimple before+ , cmd = cmdAtToSimple cmd+ , after = modelToSimple after+ , mockResp = respMockToSimple mockResp+ }++{------------------------------------------------------------------------------- Wrap and unwrap -------------------------------------------------------------------------------} -cmdAtFromSimple :: Functor (Cmd t)- => Cmd t :@ Symbolic -> NAry.Cmd (Simple t) NAry.:@ Symbolic+cmdAtFromSimple :: Functor (Cmd t) => Cmd t :@ r -> NAry.Cmd (Simple t) NAry.:@ r cmdAtFromSimple = NAry.At . SimpleCmd . fmap NAry.FlipRef . unAt -cmdAtToSimple :: Functor (Cmd t)- => NAry.Cmd (Simple t) NAry.:@ Symbolic -> Cmd t :@ Symbolic+cmdAtToSimple :: Functor (Cmd t) => NAry.Cmd (Simple t) NAry.:@ r -> Cmd t :@ r cmdAtToSimple = At . fmap (NAry.unFlipRef) . unSimpleCmd . NAry.unAt cmdMockToSimple :: Functor (Cmd t)@@ -113,6 +159,11 @@ -> NAry.Resp (Simple t) (NAry.MockHandle (Simple t)) '[RealHandle t] respMockFromSimple = SimpleResp . fmap SimpleToMock +respMockToSimple :: Functor (Resp t)+ => NAry.Resp (Simple t) (NAry.MockHandle (Simple t)) '[RealHandle t]+ -> Resp t (MockHandle t)+respMockToSimple = fmap unSimpleToMock . unSimpleResp+ respRealFromSimple :: Functor (Resp t) => Resp t (RealHandle t) -> NAry.Resp (Simple t) I '[RealHandle t]@@ -122,6 +173,12 @@ User defined values -------------------------------------------------------------------------------} +-- | State machine test+--+-- This captures the design patterns sketched in+-- <https://well-typed.com/blog/2019/01/qsm-in-depth/> for the case where there+-- is exactly one real handle. See "Test.StateMachine.Lockstep.NAry" for the+-- generalization to @n@ handles. data StateMachineTest t = ( Typeable t -- Response@@ -145,6 +202,8 @@ -- Mock state , Show (MockState t) , ToExpr (MockState t)+ -- Tags+ , Show (Tag t) ) => StateMachineTest { runMock :: Cmd t (MockHandle t) -> MockState t -> (Resp t (MockHandle t), MockState t) , runReal :: Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))@@ -153,13 +212,14 @@ , generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic)) , shrinker :: Model t Symbolic -> Cmd t :@ Symbolic -> [Cmd t :@ Symbolic] , cleanup :: Model t Concrete -> IO ()+ , tag :: [Event t Symbolic] -> [Tag t] } data Simple t type instance NAry.MockState (Simple t) = MockState t type instance NAry.RealHandles (Simple t) = '[RealHandle t]-type instance NAry.RealMonad (Simple _) = IO+type instance NAry.Tag (Simple t) = Tag t data instance NAry.Cmd (Simple _) _f _hs where SimpleCmd :: Cmd t (f h) -> NAry.Cmd (Simple t) f '[h]@@ -212,7 +272,7 @@ => ToExpr (NAry.MockHandle (Simple t) (RealHandle t)) where toExpr (SimpleToMock h) = toExpr h -fromSimple :: StateMachineTest t -> NAry.StateMachineTest (Simple t)+fromSimple :: StateMachineTest t -> NAry.StateMachineTest (Simple t) IO fromSimple StateMachineTest{..} = NAry.StateMachineTest { runMock = \cmd st -> first respMockFromSimple (runMock (cmdMockToSimple cmd) st) , runReal = \cmd -> respRealFromSimple <$> (runReal (cmdRealToSimple cmd))@@ -221,6 +281,7 @@ , generator = \m -> fmap cmdAtFromSimple <$> generator (modelToSimple m) , shrinker = \m cmd -> cmdAtFromSimple <$> shrinker (modelToSimple m) (cmdAtToSimple cmd) , cleanup = cleanup . modelToSimple+ , tag = tag . map eventToSimple } {-------------------------------------------------------------------------------
src/Test/StateMachine/Parallel.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-} ----------------------------------------------------------------------------- -- |@@ -16,6 +17,29 @@ -- 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@@ -29,10 +53,14 @@ , shrinkAndValidateParallel , shrinkCommands' , runNParallelCommands+ , runNParallelCommandsWithSetup , runParallelCommands+ , runParallelCommandsWithSetup , runParallelCommands' , runNParallelCommandsNTimes+ , runNParallelCommandsNTimesWithSetup , runParallelCommandsNTimes+ , runParallelCommandsNTimesWithSetup , runNParallelCommandsNTimes' , runParallelCommandsNTimes' , executeParallelCommands@@ -51,7 +79,7 @@ import Control.Monad (replicateM, when) import Control.Monad.Catch- (MonadMask, mask, onException)+ (MonadMask(..), ExitCase(..)) import Control.Monad.State.Strict (runStateT) import Data.Bifunctor@@ -82,6 +110,7 @@ import UnliftIO (MonadIO, MonadUnliftIO, concurrently, forConcurrently, newTChanIO)+import qualified UnliftIO as UIO import Test.StateMachine.BoxDrawer import Test.StateMachine.ConstructorName@@ -472,16 +501,24 @@ => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp- -> PropertyM m [(History cmd resp, Logic)]+ -> 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)- => StateMachine model cmd m resp+ => m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp- -> PropertyM m [(History cmd resp, Logic)]+ -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommands' = runParallelCommandsNTimes' 10 runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))@@ -489,89 +526,144 @@ => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp- -> PropertyM m [(History cmd resp, Logic)]+ -> 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, Logic)]-runParallelCommandsNTimes n sm cmds =+ -> 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)+ -> ParallelCommands cmd resp+ -> PropertyM m [(History cmd resp, model Concrete, Logic)]+runParallelCommandsNTimesWithSetup n msm cmds = replicateM n $ do- (hist, reason1, reason2) <- run (executeParallelCommands sm cmds True)- return (hist, logicReason (combineReasons [reason1, reason2]) .&& linearise sm hist)+ hchan <- newTChanIO+ ((hist, model, reason1, reason2), 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)+ return (hist, model, logicReason (combineReasons [reason1, reason2]) .&& linearise sm' hist) 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+ -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp- -> PropertyM m [(History cmd resp, Logic)]-runParallelCommandsNTimes' n sm complete cmds =+ -> PropertyM m [(History cmd resp, model Concrete, Logic)]+runParallelCommandsNTimes' n msm complete cmds = replicateM n $ do- (hist, _reason1, _reason2) <- run (executeParallelCommands sm cmds False)+ 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', linearise sm 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, Logic)]-runNParallelCommandsNTimes n sm cmds =+ -> 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- (hist, reason) <- run (executeNParallelCommands sm cmds True)- return (hist, logicReason reason .&& linearise sm hist)+ 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.- -> StateMachine model cmd m resp+ -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp- -> PropertyM m [(History cmd resp, Logic)]-runNParallelCommandsNTimes' n sm complete cmds =+ -> PropertyM m [(History cmd resp, model Concrete, Logic)]+runNParallelCommandsNTimes' n msm complete cmds = replicateM n $ do- (hist, _reason) <- run (executeNParallelCommands sm cmds True)+ 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) let hist' = completeHistory complete hist- return (hist, 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) -> Bool- -> m (History cmd resp, Reason, Reason)-executeParallelCommands sm@StateMachine{ initModel, cleanup } (ParallelCommands prefix suffixes) stopOnError =- mask $ \restore -> do- hchan <- restore newTChanIO- (reason0, (env0, _smodel, _counter, _cmodel)) <- restore (runStateT+ -> 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))- `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)- if reason0 /= Ok- then do- hist <- getChanContents hchan- cleanup $ mkModel sm $ History hist- return (History hist, reason0, reason0)- else do- (reason1, reason2, _) <- restore (go hchan (Ok, Ok, env0) suffixes)- `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)- hist <- getChanContents hchan- cleanup $ mkModel sm $ History hist- return (History hist, reason1, reason2)+ (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) where- go _hchan (res1, res2, env) [] = return (res1, res2, env)- go hchan (Ok, Ok, env) (Pair cmds1 cmds2 : pairs) = do+ go (res1, res2, env) [] = return (res1, res2, env)+ go (Ok, Ok, env) (Pair cmds1 cmds2 : pairs) = do ((reason1, (env1, _, _, _)), (reason2, (env2, _, _, _))) <- concurrently @@ -583,11 +675,11 @@ (runStateT (executeCommands sm hchan (Pid 2) CheckNothing cmds2) (env, initModel, newCounter, initModel)) case (isOK $ combineReasons [reason1, reason2], stopOnError) of (False, True) -> return (reason1, reason2, env1 <> env2)- _ -> go hchan ( reason1- , reason2- , env1 <> env2- ) pairs- go hchan (Ok, ExceptionThrown e, env) (Pair cmds1 _cmds2 : pairs) = do+ _ -> go ( reason1+ , reason2+ , env1 <> env2+ ) pairs+ go (Ok, ExceptionThrown e, env) (Pair cmds1 _cmds2 : pairs) = do -- XXX: It's possible that pre-conditions fail at this point, because -- commands may depend on references that never got created in the crashed@@ -608,22 +700,22 @@ -- (reason1, (env1, _, _, _)) <- runStateT (executeCommands sm hchan (Pid 1) CheckPrecondition cmds1) (env, initModel, newCounter, initModel)- go hchan ( reason1- , ExceptionThrown e- , env1- ) pairs- go hchan (ExceptionThrown e, Ok, env) (Pair _cmds1 cmds2 : pairs) = do+ go ( reason1+ , ExceptionThrown e+ , env1+ ) pairs+ go (ExceptionThrown e, Ok, env) (Pair _cmds1 cmds2 : pairs) = do (reason2, (env2, _, _, _)) <- runStateT (executeCommands sm hchan (Pid 2) CheckPrecondition cmds2) (env, initModel, newCounter, initModel)- go hchan ( ExceptionThrown e- , reason2- , env2- ) pairs- go _hchan out@(ExceptionThrown _, ExceptionThrown _, _env) (_ : _) = return out- go _hchan out@(PreconditionFailed {}, ExceptionThrown _, _env) (_ : _) = return out- go _hchan out@(ExceptionThrown _, PreconditionFailed {}, _env) (_ : _) = return out- go _hchan (res1, res2, _env) (Pair _cmds1 _cmds2 : _pairs) =+ go ( ExceptionThrown e+ , reason2+ , env2+ ) pairs+ go out@(ExceptionThrown _, ExceptionThrown _, _env) (_ : _) = return out+ go out@(PreconditionFailed {}, ExceptionThrown _, _env) (_ : _) = return out+ go out@(ExceptionThrown _, PreconditionFailed {}, _env) (_ : _) = return out+ go (res1, res2, _env) (Pair _cmds1 _cmds2 : _pairs) = error ("executeParallelCommands, unexpected result: " ++ show (res1, res2)) logicReason :: Reason -> Logic@@ -635,29 +727,24 @@ => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp+ -> UIO.TChan (Pid, HistoryEvent cmd resp) -> Bool- -> m (History cmd resp, Reason)-executeNParallelCommands sm@StateMachine{ initModel, cleanup } (ParallelCommands prefix suffixes) stopOnError =- mask $ \restore -> do- hchan <- restore newTChanIO- (reason0, (env0, _smodel, _counter, _cmodel)) <- restore (runStateT+ -> 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))- `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)- if reason0 /= Ok- then do- hist <- getChanContents hchan- cleanup $ mkModel sm $ History hist- return (History hist, reason0)- else do- (errors, _) <- restore (go hchan (Map.empty, env0) suffixes)- `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)- hist <- getChanContents hchan- cleanup $ mkModel sm $ History hist- return (History hist, combineReasons $ Map.elems errors)+ (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) where- go _ res [] = return res- go hchan (previousErrors, env) (suffix : rest) = do+ go res [] = return res+ go (previousErrors, env) (suffix : rest) = do when (isInvalid $ Map.elems previousErrors) $ error ("executeNParallelCommands, unexpected result: " ++ show previousErrors) @@ -674,7 +761,7 @@ newEnv = mconcat $ snd <$> res case (stopOnError, Map.null errors) of (True, False) -> return (errors, newEnv)- _ -> go hchan (errors, newEnv) rest+ _ -> go (errors, newEnv) rest combineReasons :: [Reason] -> Reason combineReasons ls = fromMaybe Ok (find (/= Ok) ls)@@ -722,10 +809,10 @@ => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions- -> [(History cmd resp, Logic)] -- ^ Output of 'runParallelCommands'.+ -> [(History cmd resp, a, Logic)] -- ^ Output of 'runParallelCommands'. -> PropertyM m ()-prettyParallelCommandsWithOpts cmds mGraphOptions =- mapM_ (\(h, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l))+prettyParallelCommandsWithOpts cmds mGraphOptions histories = do+ mapM_ (\(h, _, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l)) histories where printCounterexample hist' (VFalse ce) = do putStrLn ""@@ -753,7 +840,7 @@ => MonadIO m => Rank2.Foldable cmd => ParallelCommands cmd resp- -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'.+ -> [(History cmd resp, a, Logic)] -- ^ Output of 'runNParallelCommands'. -> PropertyM m () prettyParallelCommands cmds = prettyParallelCommandsWithOpts cmds Nothing @@ -764,10 +851,10 @@ => Rank2.Foldable cmd => NParallelCommands cmd resp -> Maybe GraphOptions- -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'.+ -> [(History cmd resp, a, Logic)] -- ^ Output of 'runNParallelCommands'. -> PropertyM m ()-prettyNParallelCommandsWithOpts cmds mGraphOptions =- mapM_ (\(h, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l))+prettyNParallelCommandsWithOpts cmds mGraphOptions histories =+ mapM_ (\(h, _, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l)) histories where printCounterexample hist' (VFalse ce) = do putStrLn ""@@ -783,7 +870,7 @@ => MonadIO m => Rank2.Foldable cmd => NParallelCommands cmd resp- -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'.+ -> [(History cmd resp, a, Logic)] -- ^ Output of 'runNParallelCommands'. -> PropertyM m () prettyNParallelCommands cmds = prettyNParallelCommandsWithOpts cmds Nothing
src/Test/StateMachine/Sequential.hs view
@@ -35,6 +35,7 @@ , ShouldShrink(..) , initValidateEnv , runCommands+ , runCommandsWithSetup , runCommands' , getChanContents , Check(..)@@ -59,7 +60,7 @@ fromException) import Control.Monad (when) import Control.Monad.Catch- (MonadCatch, MonadMask, catch, mask, onException)+ (MonadCatch(..), MonadMask (..), catch, ExitCase (..)) import Control.Monad.State.Strict (StateT, evalStateT, get, lift, put, runStateT) import Data.Bifunctor@@ -325,28 +326,36 @@ => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason)-runCommands sm cmds = run $ runCommands' sm cmds+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' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadIO m)- => StateMachine model cmd m resp+ => m (StateMachine model cmd m resp) -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason)-runCommands' sm@StateMachine { initModel, cleanup } cmds =- mask $ \restore -> do- hchan <- restore newTChanIO- (reason, (_, _, _, model)) <- restore- (runStateT- (executeCommands sm hchan (Pid 0) CheckEverything cmds)- (emptyEnvironment, initModel, newCounter, initModel))- `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)- -- if sequential execution ends normally, we have the correct and- -- deterministic final model ready, so no need to use history for cleanup.- cleanup model- -- we have cleaned up, so we can restore noe- hist <- restore $ getChanContents hchan- return (History hist, model, 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) -- We should try our best to not let this function fail, -- since it is used to cleanup resources, in parallel programs.@@ -398,8 +407,8 @@ if length vars /= length cvars then do let err = mockSemanticsMismatchError (ppShow ccmd) (ppShow vars) (ppShow cresp) (ppShow cvars)- atomically (writeTChan hchan (pid, Exception err))- return MockSemanticsMismatch+ atomically (writeTChan hchan (pid, Response cresp))+ return $ MockSemanticsMismatch err else do atomically (writeTChan hchan (pid, Response cresp)) case (check, logic (postcondition cmodel ccmd cresp)) of@@ -444,8 +453,7 @@ , "" , "Continuing to execute commands at this point could result in scope" , "errors, because we might have commands that use references (returned"- , "by `mock`) that are not available (returned by `semantics`), to avoid"- , "this please fix the mismatch."+ , "by `mock`) that are not available (returned by `semantics`)." , "" ]
src/Test/StateMachine/Types.hs view
@@ -120,7 +120,7 @@ | PostconditionFailed String | InvariantBroken String | ExceptionThrown String- | MockSemanticsMismatch+ | MockSemanticsMismatch String deriving stock (Eq, Show) isOK :: Reason -> Bool
test/Cleanup.hs view
@@ -41,6 +41,7 @@ import Test.QuickCheck.Monadic (monadicIO) import Test.StateMachine+import qualified Test.StateMachine.Types as QSM (initModel) import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Utils (liftProperty, mkModel, whenFailM)@@ -48,14 +49,14 @@ (ppShow) {------------------------------------------------------------------------------------ This example in mainly used to check how well cleanup of recourses works. In our- case recourses are files created on the @testDirectory@ (not open handles, just- files). So it is easy, by the end of the tests to test if there any any recourses+ This example in mainly used to check how well cleanup of resources works. In our+ case resources are files created on the @testDirectory@ (not open handles, just+ files). So it is easy, by the end of the tests to test if there any any resources which are not cleaned up, by the end of the tests. We also test different scenarios, like injected exceptions in semantics- (before and after the recourse is created). Tests also reveal what happens when- cleaning up a recourse for the second time is not a no-op.+ (before and after the resource is created). Tests also reveal what happens when+ cleaning up a resource for the second time is not a no-op. -----------------------------------------------------------------------------------} data Command r@@ -89,13 +90,14 @@ , 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 -> Model r+initModel :: MVar Int -> MVar Int -> String -> 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@@ -197,62 +199,63 @@ shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic] shrinker _ _ = [] -cleanup :: String -> DoubleCleanup -> Model Concrete -> IO ()-cleanup testDir dc Model{..} = do+cleanup :: DoubleCleanup -> Model Concrete -> IO ()+cleanup 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)- -- 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 ProperyM level.- cl `onException` removePathForcibly testDir+ cl `finally` removePathForcibly modelTestDir -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)+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) smUnused :: StateMachine Model Command IO Response-smUnused = sm undefined undefined undefined undefined undefined+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" prop_sequential_clean :: FinalTest -> Bug -> DoubleCleanup -> Property prop_sequential_clean testing bug dc = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do- folderId :: Word <- liftIO randomIO- let testDir = testDirectoryBase ++ "-" ++ show folderId- liftIO $ do- removePathForcibly testDir- createDirectory testDir- c <- liftIO $ newMVar 0+ counter <- liftIO $ newMVar 0 ref <- liftIO $ newMVar 0- let sm' = sm c ref testDir bug dc- (hist, model, res) <- runCommands sm' cmds- ls <- liftIO $ listDirectory testDir- liftIO $ removePathForcibly testDir+ let sm' = sm counter ref bug dc+ (hist, model, res) <- runCommandsWithSetup sm' cmds case testing of- Regular -> prettyCommands sm' hist $ checkCommandNames cmds (res === Ok)- Files -> printFiles ls `whenFailM` (ls === [])- Eq _ -> liftProperty $ mkModel sm' hist === model+ 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 prop_parallel_clean :: FinalTest -> Bug -> DoubleCleanup -> Property prop_parallel_clean testing bug dc = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do- folderId :: Word <- liftIO randomIO- let testDir = testDirectoryBase ++ "-" ++ show folderId- liftIO $ do- removePathForcibly testDir- createDirectory testDir- c <- liftIO $ newMVar 0+ counter <- liftIO $ newMVar 0 ref <- liftIO $ newMVar 0- let sm' = sm c ref testDir bug dc- ret <- runParallelCommandsNTimes 2 sm' cmds- ls <- liftIO $ listDirectory testDir- liftIO $ removePathForcibly testDir+ let sm' = sm counter ref bug dc+ ret <- runParallelCommandsNTimesWithSetup 2 sm' cmds case testing of Regular -> prettyParallelCommands cmds ret- Files -> printFiles ls `whenFailM` (ls === [])+ Files ->+ mapM_ (\(_, model, _) -> do+ ex <- property . not <$> (liftIO $ doesDirectoryExist $ modelTestDir model)+ (do+ ls <- liftIO $ listDirectory $ modelTestDir model+ printFiles ls) `whenFailM` ex) ret Eq bl -> do- let (a, b) = case mkModel sm' . fst <$> ret of+ let (a, b) = case mkModel smUnused . (\(h, _, _) -> h) <$> ret of (x : y : _) -> (x,y) _ -> error "expected at least two histories" liftProperty $ printModels a b `whenFail`@@ -260,30 +263,28 @@ prop_nparallel_clean :: Int -> FinalTest -> Bug -> DoubleCleanup -> Property prop_nparallel_clean np testing bug dc = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do- folderId :: Word <- liftIO randomIO- let testDir = testDirectoryBase ++ "-" ++ show folderId- liftIO $ do- removePathForcibly testDir- createDirectory testDir- c <- liftIO $ newMVar 0+ counter <- liftIO $ newMVar 0 ref <- liftIO $ newMVar 0- let sm' = sm c ref testDir bug dc- ret <- runNParallelCommandsNTimes 2 sm' cmds- ls <- liftIO $ listDirectory testDir- liftIO $ removePathForcibly testDir+ let sm' = sm counter ref bug dc+ ret <- runNParallelCommandsNTimesWithSetup 2 sm' cmds -- This 2 is there just to have two histories later on! case testing of Regular -> prettyNParallelCommands cmds ret- Files -> printFiles ls `whenFailM` (ls === [])+ Files ->+ mapM_ (\(_, model, _) -> do+ ex <- property . not <$> (liftIO $ doesDirectoryExist $ modelTestDir model)+ (do+ ls <- liftIO $ listDirectory $ modelTestDir model+ printFiles ls) `whenFailM` ex) ret Eq bl -> do- let (a, b) = case mkModel sm' . fst <$> ret of+ let (a, b) = case mkModel smUnused . (\(h, _, _) -> h) <$> ret of (x : y : _) -> (x,y) _ -> error "expected at least two histories" liftProperty $ printModels a b `whenFail` property (modelEquivalence bl a b) printModels :: Show1 r => Model r -> Model r -> IO ()-printModels a b =- putStrLn $ "Models are not equivalent: \n" ++ ppShow a ++ " \nand \n" ++ ppShow b+printModels a b = do+ putStrLn $ "Models are not equivalent: \n" ++ ppShow a ++ " \nand \n" ++ ppShow b printFiles :: [String] -> IO () printFiles ls' =
test/Echo.hs view
@@ -40,7 +40,7 @@ writeTVar) import Test.StateMachine-import Test.StateMachine.Types+import Test.StateMachine.Types as QC import qualified Test.StateMachine.Types.Rank2 as Rank2 ------------------------------------------------------------------------@@ -76,93 +76,97 @@ prop_echoOK :: Property prop_echoOK = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do- env <- liftIO $ mkEnv- let echoSM' = echoSM env- (hist, _, res) <- runCommands echoSM' cmds- prettyCommands echoSM' hist (res === Ok)+ (hist, _, res) <- runCommandsWithSetup echoSM cmds+ prettyCommands smUnused hist (res === Ok) -prop_echoParallelOK :: Bool -> Property-prop_echoParallelOK problem = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do- env <- liftIO $ mkEnv- let echoSM' = echoSM env- let n | problem = 2- | otherwise = 1- prettyParallelCommands cmds =<< runParallelCommandsNTimes n echoSM' cmds+prop_echoParallelOK :: Property+prop_echoParallelOK = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do+ prettyParallelCommands cmds =<< runParallelCommandsWithSetup echoSM cmds -prop_echoNParallelOK :: Int -> Bool -> Property-prop_echoNParallelOK np problem = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do- env <- liftIO $ mkEnv- let echoSM' = echoSM env- let n | problem = 2- | otherwise = 1- prettyNParallelCommands cmds =<< runNParallelCommandsNTimes n echoSM' cmds+prop_echoNParallelOK :: Int -> Property+prop_echoNParallelOK np = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do+ prettyNParallelCommands cmds =<< runNParallelCommandsWithSetup echoSM cmds smUnused :: StateMachine Model Action IO Response-smUnused = echoSM $ error "used env during command generation"+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" -echoSM :: Env -> StateMachine Model Action IO Response-echoSM env = StateMachine- { initModel = Empty- -- ^ At the beginning of time nothing was received.- , transition = mTransitions- , precondition = mPreconditions- , postcondition = mPostconditions- , generator = mGenerator+echoSM :: IO (StateMachine Model Action IO Response)+echoSM = do+ env <- mkEnv+ pure $ StateMachine+ { initModel = Empty -- At the beginning of time nothing was received.+ , transition = transitions+ , precondition = preconditions+ , postcondition = postconditions+ , QC.generator = Echo.generator , invariant = Nothing- , shrinker = mShrinker- , semantics = mSemantics- , mock = mMock+ , QC.shrinker = Echo.shrinker+ , QC.semantics = Echo.semantics env+ , QC.mock = Echo.mock , cleanup = noCleanup }- 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.- mPreconditions :: Model Symbolic -> Action Symbolic -> Logic- mPreconditions _ _ = Top+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" - -- | 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+-- | There are no preconditions for this model.+preconditions :: Model Symbolic -> Action Symbolic -> Logic+preconditions _ _ = Top - -- | Generator for symbolic actions.- mGenerator :: Model Symbolic -> Maybe (Gen (Action Symbolic))- mGenerator _ = Just $ oneof- [ In <$> arbitrary- , return Echo- ]+-- | 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 - -- | Trivial shrinker.- mShrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]- mShrinker _ _ = []+-- | Generator for symbolic actions.+generator :: Model Symbolic -> Maybe (Gen (Action Symbolic))+generator _ = Just $ oneof+ [ In <$> arbitrary+ , return Echo+ ] - -- | 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+-- | Trivial shrinker.+shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]+shrinker _ _ = [] - -- | 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)+-- | 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++-- | 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) deriving anyclass instance ToExpr (Model Concrete)
test/IORefs.hs view
@@ -53,6 +53,8 @@ instance ToExpr (MockHandle (T a)) instance ToExpr (RealHandle (T a)) +type instance Tag (T _) = TagCmd+ {------------------------------------------------------------------------------- Interpreters -------------------------------------------------------------------------------}@@ -105,6 +107,23 @@ genHandle = elements (map fst hs) {-------------------------------------------------------------------------------+ Tagging++ We just label with the name of the command, for now.+-------------------------------------------------------------------------------}++data TagCmd = TagNew | TagRead | TagUpdate+ deriving stock (Show)++tagCmds :: [Event (T Int) Symbolic] -> [TagCmd]+tagCmds = map (aux . unAt . cmd)+ where+ aux :: Cmd (T Int) h -> TagCmd+ aux New = TagNew+ aux (Read _) = TagRead+ aux (Update _) = TagUpdate++{------------------------------------------------------------------------------- Wrapping it all up NOTE: The parallel property will fail (intentional race condition).@@ -119,6 +138,7 @@ , runMock = IORefs.runMock 0 (+1) , runReal = IORefs.runReal 0 (+1) , cleanup = \_ -> return ()+ , tag = tagCmds } prop_IORefs_sequential :: Property
test/MemoryReference.hs view
@@ -223,7 +223,7 @@ prop_parallel' :: Bug -> Property prop_parallel' bug = forAllParallelCommands sm' Nothing $ \cmds -> monadicIO $ do- prettyParallelCommands cmds =<< runParallelCommands' sm' complete cmds+ prettyParallelCommands cmds =<< runParallelCommands' (pure sm') complete cmds where sm' = sm bug complete :: Command Concrete -> Response Concrete
test/Mock.hs view
@@ -19,8 +19,6 @@ where import Control.Concurrent-import Control.Monad.IO.Class- (liftIO) import GHC.Generics (Generic, Generic1) import Prelude@@ -96,29 +94,31 @@ shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic] shrinker _ _ = [] -sm :: MVar Int -> StateMachine Model Command IO Response-sm counter = StateMachine initModel transition precondition postcondition+sm :: IO (StateMachine Model Command IO Response)+sm = do+ counter <- newMVar 0+ pure $ StateMachine initModel transition precondition postcondition Nothing generator shrinker (semantics counter) mock noCleanup smUnused :: StateMachine Model Command IO Response-smUnused = sm undefined+smUnused = StateMachine initModel transition precondition postcondition+ Nothing generator shrinker e mock noCleanup+ where+ e = error "SUT must not be used" prop_sequential_mock :: Property prop_sequential_mock = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do- counter <- liftIO $ newMVar 0- (hist, _model, res) <- runCommands (sm counter) cmds+ (hist, _model, res) <- runCommandsWithSetup sm cmds prettyCommands smUnused hist (res === Ok) prop_parallel_mock :: Property prop_parallel_mock = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do- counter <- liftIO $ newMVar 0- ret <- runParallelCommandsNTimes 1 (sm counter) cmds+ ret <- runParallelCommandsWithSetup sm 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- counter <- liftIO $ newMVar 0- ret <- runNParallelCommandsNTimes 1 (sm counter) cmds+ ret <- runNParallelCommandsWithSetup sm cmds prettyNParallelCommandsWithOpts cmds opts ret where opts = Just $ GraphOptions "mock-np-test-output.png" Png
test/ProcessRegistry.hs view
@@ -315,7 +315,7 @@ Exit -> Top postcondition :: Model Concrete -> Action Concrete -> Response Concrete -> Logic-postcondition Model {..} act (Response (Left err)) = case act of+postcondition _model act (Response (Left err)) = case act of BadRegister _name _pid -> Top BadUnregister _name -> Top _ -> Bot .// show err
test/RQlite.hs view
@@ -34,7 +34,7 @@ import Data.Foldable import Data.Functor.Classes import Data.Kind-import Data.List+import qualified Data.List as L import Data.Map (Map) import qualified Data.Map as M@@ -278,7 +278,7 @@ ------------------------ sameElements :: Eq a => [a] -> [a] -> Bool-sameElements x y = null (x \\ y) && null (y \\ x)+sameElements x y = null (x L.\\ y) && null (y L.\\ x) type NodeRef = Reference Container @@ -562,7 +562,7 @@ Delay _ -> Top postcondition :: Model Concrete -> At Cmd Concrete -> At Resp Concrete -> Logic-postcondition m@Model{..} cmd resp =+postcondition m cmd resp = toMock (eventAfter ev) resp .== eventMockResp ev where ev = lockstep m cmd resp@@ -640,57 +640,47 @@ UnPause {} -> return unitResp Delay {} -> return unitResp -sm :: MVar Int -> Maybe Level -> StateMachine Model (At Cmd) IO (At Resp)-sm counter lvl = StateMachine initModel transition precondition postcondition+sm :: Maybe Level -> IO (StateMachine Model (At Cmd) IO (At Resp))+sm lvl = do+ createRQNetworks+ removePathForcibly testPath+ createDirectory testPath+ threadDelay 10000+ counter <- newMVar 0+ pure $ StateMachine initModel transition precondition postcondition Nothing (generatorImpl lvl) shrinker (semantics counter) mock garbageCollect +smUnused :: Maybe Level -> StateMachine Model (At Cmd) IO (At Resp)+smUnused lvl = StateMachine initModel transition precondition postcondition+ Nothing (generatorImpl lvl) shrinker e mock garbageCollect+ where+ e = error "SUT must not be used"+ prop_sequential_rqlite :: Maybe Level -> Property prop_sequential_rqlite lvl =- forAllCommands (sm undefined lvl) (Just 7) $ \cmds -> checkCommandNames cmds $ monadicIO $ do- liftIO $ do- createRQNetworks- removePathForcibly testPath- createDirectory testPath- threadDelay 10000- c <- liftIO $ newMVar 0- (hist, _, res) <- runCommands (sm c lvl) cmds- prettyCommands (sm undefined lvl) hist $ res === Ok+ forAllCommands (smUnused lvl) (Just 7) $ \cmds -> checkCommandNames cmds $ monadicIO $ do+ (hist, _, res) <- runCommandsWithSetup (sm lvl) cmds+ prettyCommands (smUnused lvl) hist $ res === Ok prop_parallel_rqlite :: Maybe Level -> Property prop_parallel_rqlite lvl =- forAllParallelCommands (sm undefined lvl) (Just 7) $ \cmds -> checkCommandNamesParallel cmds $ monadicIO $ do- liftIO $ do- createRQNetworks- removePathForcibly testPath- createDirectory testPath- threadDelay 10000- c <- liftIO $ newMVar 0+ forAllParallelCommands (smUnused lvl) (Just 7) $ \cmds -> checkCommandNamesParallel cmds $ monadicIO $ prettyParallelCommandsWithOpts cmds (Just $ GraphOptions "rqlite-test-output.png" Png)- =<< runParallelCommandsNTimes 2 (sm c lvl) cmds+ =<< runParallelCommandsNTimesWithSetup 2 (sm lvl) cmds prop_nparallel_rqlite :: Int -> Maybe Level -> Property prop_nparallel_rqlite np lvl =- forAllNParallelCommands (sm undefined lvl) np $ \cmds ->- monadicIO $ do- liftIO $ do- removePathForcibly testPath- createDirectory testPath- threadDelay 10000- c <- liftIO $ newMVar 0+ forAllNParallelCommands (smUnused lvl) np $ \cmds -> monadicIO $ do prettyNParallelCommandsWithOpts cmds (Just $ GraphOptions "rqlite-test-output.png" Png)- =<< runNParallelCommandsNTimes 1 (sm c lvl) cmds+ =<< runNParallelCommandsNTimesWithSetup 1 (sm lvl) cmds runCmds :: ParallelCommandsF [] (At Cmd) (At Resp) -> Property runCmds cmds = withMaxSuccess 1 $ noShrinking $ monadicIO $ do- liftIO $ do- removePathForcibly testPath- createDirectory testPath- c <- liftIO $ newMVar 0- ls <- runNParallelCommandsNTimes 1 (sm c $ Just Weak) cmds+ ls <- runNParallelCommandsNTimesWithSetup 1 (sm $ Just Weak) cmds prettyNParallelCommandsWithOpts cmds (Just $ GraphOptions "rqlite-test-output.png" Png) ls- liftIO $ print $ fst $ head ls- liftIO $ print $ interleavings $ unHistory $ fst $ head ls+ liftIO $ print $ (\(a, _, _) -> a) $ head ls+ liftIO $ print $ interleavings $ unHistory $ (\(a, _, _) -> a) $ head ls garbageCollect :: Model Concrete -> IO () garbageCollect (Model _ nodes) =@@ -731,7 +721,7 @@ joinNode avoid0 ndState = case snd <$> getRunning ndState of [] -> Nothing- rs -> Just $ case (elem 0 rs, delete 0 rs, avoid0) of+ rs -> Just $ case (elem 0 rs, L.delete 0 rs, avoid0) of (False, _, _) -> head rs (True, _, False) -> 0 (True, rs', True) -> head rs'
test/SQLite.hs view
@@ -38,13 +38,11 @@ import Data.Functor.Classes import Data.Kind (Type)-import Data.List hiding- (insert) import Data.Maybe (fromMaybe) import Data.Pool import Data.Text- (Text)+ (Text, pack) import Data.TreeDiff.Expr import Database.Persist import Database.Persist.Sqlite@@ -269,8 +267,16 @@ deriving anyclass instance ToExpr DBModel deriving anyclass instance ToExpr (Model Concrete) -sm :: MonadIO m => String -> AsyncWithPool SqlBackend -> MVar () -> StateMachine Model (At Cmd) m (At Resp)-sm folder poolBackend lock = StateMachine {+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 { initModel = initModelImpl , transition = transitionImpl , precondition = preconditionImpl@@ -280,14 +286,30 @@ , shrinker = shrinkerImpl , semantics = semanticsImpl poolBackend lock , mock = mockImpl- , cleanup = clean folder+ , cleanup = \model -> do+ liftIO $ closeSqlAsyncPool poolBackend+ clean folder model } smUnused :: StateMachine Model (At Cmd) IO (At Resp)-smUnused = sm undefined undefined undefined+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" generatorImpl :: Model Symbolic -> Maybe (Gen (At Cmd Symbolic))-generatorImpl Model {..} = Just $ At <$>+generatorImpl _model = Just $ At <$> frequency [ (3, Insert <$> arbitrary) , (3, SelectList <$> arbitrary) ]@@ -319,31 +341,14 @@ prop_sequential_sqlite :: Property prop_sequential_sqlite = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do- liftIO $ do- removePathForcibly "sqlite-seq"- createDirectory "sqlite-seq"- db <- liftIO $ runNoLoggingT $ createSqliteAsyncPool "sqlite-seq/persons.db" 5- _ <- liftIO $ flip runSqlAsyncWrite db $ do- _ <- runMigrationQuiet $ migrate entityDefs $ entityDef (Nothing :: Maybe Person)- runMigrationQuiet $ migrate entityDefs $ entityDef (Nothing :: Maybe Car)- lock <- liftIO $ newMVar ()- (hist, _model, res) <- runCommands (sm "sqlite-seq" db lock) cmds+ (hist, _model, res) <- runCommandsWithSetup (sm "sqlite-seq") cmds prettyCommands smUnused hist $ res === Ok prop_parallel_sqlite :: Property prop_parallel_sqlite = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do- liftIO $ do- removePathForcibly "sqlite-par"- createDirectory "sqlite-par"- qBackend <- liftIO $ runNoLoggingT $ createSqliteAsyncPool "sqlite-par/persons.db" 5- _ <- liftIO $ flip runSqlAsyncWrite qBackend $ do- _ <- runMigrationQuiet $ migrate entityDefs $ entityDef (Nothing :: Maybe Person)- runMigrationQuiet $ migrate entityDefs $ entityDef (Nothing :: Maybe Car)- lock <- liftIO $ newMVar ()- ret <- runParallelCommandsNTimes 1 (sm "sqlite-par" qBackend lock) cmds+ ret <- runParallelCommandsNTimesWithSetup 1 (sm "sqlite-par") cmds prettyParallelCommandsWithOpts cmds (Just $ GraphOptions "sqlite.jpeg" Jpeg) ret- liftIO $ closeSqlAsyncPool qBackend instance Bifoldable t => Rank2.Foldable (At t) where foldMap = \f (At x) -> bifoldMap (app f) (app f) x
test/ShrinkingProps.hs view
@@ -707,7 +707,7 @@ sfxs = (\c -> [c]) . QSM.Commands <$> cmdsChucks nParallelCmd = QSM.ParallelCommands {prefix = QSM.Commands px, suffixes = sfxs} res <- runNParallelCommandsNTimes 1 sm nParallelCmd- let (hist', _ret) = unzip res+ let (hist', _ret) = unzip [ (a, c) | (a, _, c) <- res ] let events = snd <$> (QSM.unHistory hist) events' = snd <$> (concat (QSM.unHistory <$> hist')) return $ cmpList equalH events' events
test/Spec.hs view
@@ -108,13 +108,15 @@ $ 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" $ prop_nparallel_clean 3 Regular Cleanup.NoBug ReDo+ , testProperty "3-threadsRegular"+ $ expectFailure $ 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" $ prop_nparallel_clean 3 Files Cleanup.NoBug ReDo+ , testProperty "3-threadsFiles"+ $ expectFailure $ 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@@ -126,12 +128,13 @@ , testGroup "SQLite" [ testProperty "Parallel" prop_parallel_sqlite ]- , testGroup "Rqlite"- [ whenDocker docker0 "rqlite" $ testProperty "parallel" $ withMaxSuccess 10 $ prop_parallel_rqlite (Just Weak)+ -- 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@@ -187,15 +190,9 @@ ] , testGroup "Echo" [ testProperty "Sequential" prop_echoOK- , testProperty "ParallelOk" (prop_echoParallelOK False)- , testProperty "ParallelBad" -- See issue #218.- (expectFailure (prop_echoParallelOK True))- , testProperty "2-Parallel" (prop_echoNParallelOK 2 False)- , testProperty "3-Parallel" (prop_echoNParallelOK 3 False)- , testProperty "Parallel bad, 2 threads, see issue #218"- (expectFailure (prop_echoNParallelOK 2 True))- , testProperty "Parallel bad, 3 threads, see issue #218"- (expectFailure (prop_echoNParallelOK 3 True))+ , testProperty "Parallel" prop_echoParallelOK+ , testProperty "2-Parallel" (prop_echoNParallelOK 2)+ , testProperty "3-Parallel" (prop_echoNParallelOK 3) ] , testGroup "ProcessRegistry" [ testProperty "Sequential" (prop_processRegistry (statsDb "processRegistry"))
test/TicketDispenser.hs view
@@ -194,39 +194,40 @@ run lock liftIO $ 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+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) -smUnused :: SharedExclusive -> StateMachine Model Action IO Response-smUnused se = sm se (error "dblock used during command creation")+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" -- Sequentially the model is consistent (even though the lock is -- shared). prop_ticketDispenser :: Property prop_ticketDispenser =- forAllCommands (smUnused Shared) Nothing $ \cmds -> monadicIO $- withDbLock $ \ioLock -> do- let sm' = sm Shared ioLock- (hist, _, res) <- runCommands sm' cmds- prettyCommands sm' hist $+ forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do+ (hist, _, res) <- runCommandsWithSetup (sm Shared) cmds+ prettyCommands smUnused hist $ checkCommandNames cmds (res === Ok) prop_ticketDispenserParallel :: SharedExclusive -> Property prop_ticketDispenserParallel se =- forAllParallelCommands (smUnused se) Nothing $ \cmds -> monadicIO $- withDbLock $ \ioLock -> do- let sm' = sm se ioLock- prettyParallelCommands cmds =<< runParallelCommandsNTimes 100 sm' cmds+ forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do+ let sm' = sm se+ prettyParallelCommands cmds =<< runParallelCommandsNTimesWithSetup 100 sm' cmds prop_ticketDispenserNParallel :: SharedExclusive -> Int -> Property prop_ticketDispenserNParallel se np =- forAllNParallelCommands (smUnused se) np $ \cmds -> monadicIO $- withDbLock $ \ioLock -> do- let sm' = sm se ioLock- prettyNParallelCommands cmds =<< runNParallelCommands sm' cmds+ forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do+ let sm' = sm se+ prettyNParallelCommands cmds =<< runNParallelCommandsWithSetup sm' cmds -- So long as the file locks are exclusive, i.e. not shared, the -- parallel property passes.