quickcheck-state-machine 0.4.0 → 0.4.1
raw patch · 20 files changed
+362/−103 lines, 20 filesdep +doctestdep +tasty-hunitdep ~stm
Dependencies added: doctest, tasty-hunit
Dependency ranges changed: stm
Files
- CHANGELOG.md +7/−0
- README.md +8/−19
- quickcheck-state-machine.cabal +5/−1
- src/Test/StateMachine.hs +1/−2
- src/Test/StateMachine/Logic.hs +18/−7
- src/Test/StateMachine/Parallel.hs +4/−3
- src/Test/StateMachine/Sequential.hs +1/−21
- src/Test/StateMachine/Types.hs +2/−4
- src/Test/StateMachine/Types/Environment.hs +1/−1
- src/Test/StateMachine/Types/History.hs +15/−1
- src/Test/StateMachine/Types/References.hs +1/−1
- src/Test/StateMachine/Utils.hs +1/−1
- src/Test/StateMachine/Z.hs +61/−7
- test/CircularBuffer.hs +1/−2
- test/CrudWebserverDb.hs +9/−14
- test/DieHard.hs +3/−4
- test/Echo.hs +184/−0
- test/MemoryReference.hs +1/−1
- test/Spec.hs +37/−11
- test/TicketDispenser.hs +2/−3
CHANGELOG.md view
@@ -1,3 +1,10 @@+#### 0.4.1 (2018-8-31)++ * Minor fixes release:++ - Fix broken link and code in README;+ - Disable web server tests when docker isn't available (issue #222).+ #### 0.4.0 (2018-8-21) * Major rewrite, addressing many issues:
README.md view
@@ -118,16 +118,9 @@ transition m@(Model model) cmd resp = case (cmd, resp) of (Create, Created ref) -> Model ((ref, 0) : model) (Read _, ReadValue _) -> m- (Write ref x, Written) -> Model ((ref, x) : filter ((/= ref) . fst) model)+ (Write ref x, Written) -> Model (update ref x model) (Increment ref, Incremented) -> case lookup ref model of- Just i -> Model ((ref, succ i) : filter ((/= ref) . fst) model)-transition :: Ord1 v => Model v -> Action v resp -> v resp -> Model v-transition (Model m) New ref = Model (m ++ [(Reference ref, 0)])-transition m (Read _) _ = m-transition (Model m) (Write ref i) _ = Model (update ref i m)-transition (Model m) (Inc ref) _ = Model (update ref (old + 1) m)- where- Just old = lookup ref m+ Just i -> Model (update ref (succ i) model) update :: Eq a => a -> b -> [(a, b)] -> [(a, b)] update ref i m = (ref, i) : filter ((/= ref) . fst) m@@ -177,7 +170,7 @@ ```haskell sm :: Bug -> StateMachine Model Command IO Response sm bug = StateMachine initModel transition precondition postcondition- Nothing Nothing generator Nothing shrinker (semantics bug) id mock+ Nothing generator Nothing shrinker (semantics bug) mock ``` We can now define a sequential property as follows.@@ -300,7 +293,7 @@ We shall come back to this example below, but if your are impatient you can find the full source code-[here](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MutableReference.hs).+[here](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MemoryReference.hs). ### How it works @@ -378,13 +371,9 @@ * Mutable reference- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MutableReference.hs) --+ [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MemoryReference.hs) -- this is a bigger example that shows both how the sequential property can- find normal bugs, and how the parallel property can find race conditions.- Several metaproperties, that for example check if the counterexamples are- minimal, are specified in a- separate- [module](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MutableReference/Prop.hs);+ find normal bugs, and how the parallel property can find race conditions; * Circular buffer [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/CircularBuffer.hs)@@ -478,7 +467,7 @@ author, Jean-Raymond Abrial, himself: + [Lecture 1](https://www.youtube.com/watch?v=2GP1pJINVT4):- introduction to modeling and Event-B (chapter 1 of the+ introduction to modelling and Event-B (chapter 1 of the book) and start of "controlling cars on bridge" example (chapter 2); @@ -505,7 +494,7 @@ The books contain general advice how to model systems using state machines, and are hence relevant to us. For shorter texts on why state machines are- important for modeling, see:+ important for modelling, see: - Lamport's [*Computation and State Machines*](https://www.microsoft.com/en-us/research/publication/computation-state-machines/);
quickcheck-state-machine.cabal view
@@ -1,6 +1,6 @@ cabal-version: >=1.10 name: quickcheck-state-machine-version: 0.4.0+version: 0.4.1 license: BSD3 license-file: LICENSE copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;@@ -74,6 +74,7 @@ CircularBuffer CrudWebserverDb DieHard+ Echo MemoryReference TicketDispenser default-language: Haskell2010@@ -86,6 +87,7 @@ base >=4.11.1.0, bytestring >=0.10.8.2, directory >=1.3.1.5,+ doctest >=0.16.0, filelock >=0.1.1.2, filepath >=1.4.2, http-client >=0.5.13.1,@@ -107,9 +109,11 @@ servant >=0.14.1, servant-client >=0.14, servant-server >=0.14.1,+ stm >=2.4.5.0, strict >=0.3.2, string-conversions >=0.4.0.1, tasty >=1.1.0.2,+ tasty-hunit >=0.10.0.1, tasty-quickcheck >=0.10, text >=1.2.3.0, tree-diff >=0.0.1,
src/Test/StateMachine.hs view
@@ -4,7 +4,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -18,7 +18,6 @@ ( -- * Sequential property combinators forAllCommands , transitionMatrix- , modelCheck , runCommands , prettyCommands , checkCommandNames
src/Test/StateMachine/Logic.hs view
@@ -7,7 +7,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -35,6 +35,9 @@ , elem , notElem , (.//)+ , (.&&)+ , (.||)+ , (.=>) , forall , exists )@@ -46,10 +49,6 @@ ------------------------------------------------------------------------ -infixr 1 :=>-infixr 2 :||-infixr 3 :&&- data Logic = Bot | Top@@ -188,9 +187,12 @@ infix 5 .<= infix 5 .> infix 5 .>=-infix 5 `elem`-infix 5 `notElem`+infix 8 `elem`+infix 8 `notElem` infixl 4 .//+infixr 3 .&&+infixr 2 .||+infixr 1 .=> (.==) :: (Eq a, Show a) => a -> a -> Logic x .== y = Predicate (x :== y)@@ -218,6 +220,15 @@ (.//) :: Logic -> String -> Logic l .// s = Annotate s l++(.&&) :: Logic -> Logic -> Logic+(.&&) = (:&&)++(.||) :: Logic -> Logic -> Logic+(.||) = (:||)++(.=>) :: Logic -> Logic -> Logic+(.=>) = (:=>) forall :: Show a => [a] -> (a -> Logic) -> Logic forall = Forall
src/Test/StateMachine/Parallel.hs view
@@ -9,7 +9,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -26,6 +26,7 @@ , prop_splitCombine , runParallelCommands , runParallelCommandsNTimes+ , executeParallelCommands , linearise , toBoxDrawings , prettyParallelCommands@@ -55,7 +56,7 @@ ((<>)) import Data.Set (Set)-import qualified Data.Set as S+import qualified Data.Set as S import Data.Tree (Tree(Node)) import GHC.Generics@@ -77,7 +78,7 @@ (boolean) import Test.StateMachine.Sequential import Test.StateMachine.Types-import qualified Test.StateMachine.Types.Rank2 as Rank2+import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Utils ------------------------------------------------------------------------
src/Test/StateMachine/Sequential.hs view
@@ -12,7 +12,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -32,7 +32,6 @@ , liftShrinkCommand , validCommands , filterMaybe- , modelCheck , runCommands , getChanContents , executeCommands@@ -242,25 +241,6 @@ Just ih -> return (Just (Command cmd vars : ih)) else return Nothing--modelCheck :: forall model cmd resp m. Monad m => StateMachine model cmd m resp- -> Commands cmd- -> PropertyM m Reason -- XXX: (History cmd, model Symbolic, Reason)-modelCheck StateMachine { initModel, transition, precondition, spostcondition, mock }- = run . return . go initModel newCounter . unCommands- where- go :: model Symbolic -> Counter -> [Command cmd] -> Reason- go _ _ [] = Ok- go m counter (Command cmd _vars : cmds)- | not (boolean (precondition m cmd)) = PreconditionFailed- | otherwise =- let (resp, counter') = runGenSym (mock m cmd) counter in- case logic (fromMaybe err spostcondition m cmd resp) of- VTrue -> go (transition m cmd resp) counter' cmds- VFalse ce -> PostconditionFailed (show ce)- where- err = error "modelCheck: Symbolic post-condition must be \- \ specificed in state machine in order to do model checking." runCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadCatch m, MonadBaseControl IO m)
src/Test/StateMachine/Types.hs view
@@ -14,7 +14,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -47,7 +47,7 @@ (Set) import Prelude import Test.QuickCheck- (Gen, Property)+ (Gen) import Test.StateMachine.Logic import Test.StateMachine.Types.Environment@@ -62,13 +62,11 @@ , transition :: forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r , precondition :: model Symbolic -> cmd Symbolic -> Logic , postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic- , spostcondition :: Maybe (model Symbolic -> cmd Symbolic -> resp Symbolic -> Logic) , invariant :: Maybe (model Concrete -> Logic) , generator :: model Symbolic -> Gen (cmd Symbolic) , distribution :: Maybe (Matrix Int) , shrinker :: cmd Symbolic -> [cmd Symbolic] , semantics :: cmd Concrete -> m (resp Concrete)- , runner :: m Property -> IO Property , mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) }
src/Test/StateMachine/Types/Environment.hs view
@@ -8,7 +8,7 @@ -- Copyright : (C) 2017, Jacob Stanley -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --
src/Test/StateMachine/Types/History.hs view
@@ -1,10 +1,12 @@+{-# LANGUAGE StandaloneDeriving #-}+ ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Types.History -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -37,6 +39,12 @@ newtype History cmd resp = History { unHistory :: History' cmd resp } +deriving instance (Eq (cmd Concrete), Eq (resp Concrete)) =>+ Eq (History cmd resp)++deriving instance (Show (cmd Concrete), Show (resp Concrete)) =>+ Show (History cmd resp)+ type History' cmd resp = [(Pid, HistoryEvent cmd resp)] newtype Pid = Pid { unPid :: Int }@@ -45,6 +53,12 @@ data HistoryEvent cmd resp = Invocation !(cmd Concrete) !(Set Var) | Response !(resp Concrete)++deriving instance (Eq (cmd Concrete), Eq (resp Concrete)) =>+ Eq (HistoryEvent cmd resp)++deriving instance (Show (cmd Concrete), Show (resp Concrete)) =>+ Show (HistoryEvent cmd resp) ------------------------------------------------------------------------
src/Test/StateMachine/Types/References.hs view
@@ -11,7 +11,7 @@ -- Copyright : (C) 2017, Jacob Stanley -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --
src/Test/StateMachine/Utils.hs view
@@ -8,7 +8,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --
src/Test/StateMachine/Z.hs view
@@ -1,10 +1,12 @@+{-# LANGUAGE TypeOperators #-}+ ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Z -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : portable --@@ -15,12 +17,16 @@ ----------------------------------------------------------------------------- module Test.StateMachine.Z- ( union+ ( cons+ , union , intersect , isSubsetOf , (~=) , Rel , Fun+ , (:<->)+ , (:->)+ , (:/->) , empty , identity , singleton@@ -50,31 +56,60 @@ , isTotalSurj , isBijection , (!)+ , (!?) , (.%) , (.!) , (.=) ) where import qualified Data.List as L-import qualified Prelude as P import Prelude hiding (elem, notElem)+import qualified Prelude as P import Test.StateMachine.Logic ------------------------------------------------------------------------ +infixr 6 `union`+infixr 7 `intersect`+infix 5 `isSubsetOf`+infix 5 ~=+infixr 4 <|+infixl 4 |>+infixr 4 <-|+infixl 4 |->+infixr 4 <++infixl 4 <**>+infixl 4 <||>+infixr 4 .%+infixr 9 .!+infix 4 .=++------------------------------------------------------------------------++cons :: a -> [a] -> [a]+cons = (:)+ union :: Eq a => [a] -> [a] -> [a] union = L.union intersect :: Eq a => [a] -> [a] -> [a] intersect = L.intersect +-- | Subset.+--+-- >>> boolean ([1, 2] `isSubsetOf` [3, 2, 1])+-- True isSubsetOf :: (Eq a, Show a) => [a] -> [a] -> Logic r `isSubsetOf` s = r .== r `intersect` s +-- | Set equality.+--+-- >>> boolean ([1, 1, 2] ~= [2, 1])+-- True (~=) :: (Eq a, Show a) => [a] -> [a] -> Logic-xs ~= ys = xs `isSubsetOf` ys :&& ys `isSubsetOf` xs+xs ~= ys = xs `isSubsetOf` ys .&& ys `isSubsetOf` xs ------------------------------------------------------------------------ @@ -84,6 +119,16 @@ -- | (Partial) functions. type Fun a b = Rel a b +infixr 1 :->+type a :-> b = Fun a b++-- Partial function.+infixr 1 :/->+type a :/-> b = Fun a b++infixr 1 :<->+type a :<-> b = Rel a b+ ------------------------------------------------------------------------ empty :: Rel a b@@ -149,9 +194,15 @@ -- | Codomain substraction. ----- >>> [ ('a', "apa"), ('b', "bepa") ] |-> ["apa"]+-- >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa"]+-- [('b',"bepa"),('c',"cepa")]+--+-- >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa", "cepa"] -- [('b',"bepa")] --+-- >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa"] |-> ["cepa"]+-- [('b',"bepa")]+-- (|->) :: Eq b => Rel a b -> [b] -> Rel a b xys |-> ys = [ (x, y) | (x, y) <- xys, y `P.notElem` ys ] @@ -168,7 +219,7 @@ -- [('a',"apa"),('b',"bepa")] -- (<+) :: (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b-r <+ s = domain s <-| r `union` s+r <+ s = (domain s <-| r) `union` s -- | Direct product. (<**>) :: Eq a => Rel a b -> Rel a c -> Rel a (b, c)@@ -223,7 +274,10 @@ (!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b f ! x = maybe (error msg) Prelude.id (lookup x f) where- msg = "!: failed to lookup `" ++ show x ++ "' in `" ++ show f ++ "'"+ msg = "!: failed to lookup `" ++ show x ++ "' in `" ++ show f ++ "'"++(!?) :: Eq a => Fun a b -> a -> Maybe b+f !? x = lookup x f (.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a b (f, x) .% g = f .! x .= g (f ! x)
test/CircularBuffer.hs view
@@ -281,8 +281,7 @@ sm :: Version -> Bugs -> StateMachine Model Action IO Response sm version bugs = StateMachine initModel transition (precondition bugs) postcondition- Nothing Nothing (generator version) Nothing- shrinker (semantics bugs) P.id mock+ Nothing (generator version) Nothing shrinker (semantics bugs) mock -- | Property parameterized by spec version and bugs. prepropcircularBuffer :: Version -> Bugs -> Property
test/CrudWebserverDb.hs view
@@ -25,7 +25,7 @@ -- (C) 2017-2018, Stevan Andjelkovic -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -349,21 +349,18 @@ ------------------------------------------------------------------------ -sm :: Warp.Port -> StateMachine Model Action (ReaderT ClientEnv IO) Response-sm port = StateMachine initModel transitions preconditions postconditions- Nothing Nothing generator Nothing- shrinker semantics (runner port) mock+sm :: StateMachine Model Action (ReaderT ClientEnv IO) Response+sm = StateMachine initModel transitions preconditions postconditions+ Nothing generator Nothing shrinker semantics mock ------------------------------------------------------------------------ -- * Sequential property prop_crudWebserverDb :: Int -> Property prop_crudWebserverDb port =- forAllCommands sm' Nothing $ \cmds -> monadic (ioProperty . runner port) $ do- (hist, _, res) <- runCommands sm' cmds- prettyCommands sm' hist (res === Ok)- where- sm' = sm port+ forAllCommands sm Nothing $ \cmds -> monadic (ioProperty . runner port) $ do+ (hist, _, res) <- runCommands sm cmds+ prettyCommands sm hist (res === Ok) withCrudWebserverDb :: Bug -> Int -> IO () -> IO () withCrudWebserverDb bug port run =@@ -390,10 +387,8 @@ prop_crudWebserverDbParallel :: Int -> Property prop_crudWebserverDbParallel port =- forAllParallelCommands sm' $ \cmds -> monadic (ioProperty . runner port) $ do- prettyParallelCommands cmds =<< runParallelCommandsNTimes 30 sm' cmds- where- sm' = sm port+ forAllParallelCommands sm $ \cmds -> monadic (ioProperty . runner port) $ do+ prettyParallelCommands cmds =<< runParallelCommandsNTimes 30 sm cmds demoRace' :: Int -> IO () demoRace' port = withCrudWebserverDb Race port
test/DieHard.hs view
@@ -13,7 +13,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -111,7 +111,7 @@ -- actually does contain 4 liters, then a minimal counter example will -- be presented -- this will be our solution. -postconditions :: Model r -> Command r -> Response r -> Logic+postconditions :: Model Concrete -> Command Concrete -> Response Concrete -> Logic postconditions s c r = bigJug (transitions s c r) ./= 4 ------------------------------------------------------------------------@@ -154,8 +154,7 @@ sm :: StateMachine Model Command IO Response sm = StateMachine initModel transitions preconditions postconditions- (Just postconditions) Nothing- generator Nothing shrinker semantics id mock+ Nothing generator Nothing shrinker semantics mock prop_dieHard :: Property prop_dieHard = forAllCommands sm Nothing $ \cmds -> monadicIO $ do
+ test/Echo.hs view
@@ -0,0 +1,184 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneDeriving #-}++-----------------------------------------------------------------------------+-- |+-- Module : Echo+-- Copyright : (C) 2018, Damian Nadales+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+------------------------------------------------------------------------++module Echo+ ( mkEnv+ , prop_echoOK+ , prop_echoParallelOK+ )+ where++import Control.Concurrent.STM+ (atomically)+import Control.Concurrent.STM.TVar+ (TVar, newTVarIO, readTVar, writeTVar)+import Data.TreeDiff+ (ToExpr)+import GHC.Generics+ (Generic, Generic1)+import Prelude+import Test.QuickCheck+ (Gen, Property, arbitrary, oneof, (===))+import Test.QuickCheck.Monadic+ (monadicIO)++import Test.StateMachine+import Test.StateMachine.Types+import qualified Test.StateMachine.Types.Rank2 as Rank2++------------------------------------------------------------------------++-- | Echo API.++data Env = Env+ { _buf :: TVar (Maybe String) }++-- | Create a new environment.+mkEnv :: IO Env+mkEnv = Env <$> newTVarIO Nothing++-- | Input a string. Returns 'True' iff the buffer was empty and the given+-- string was added to it.+input :: Env -> String -> IO Bool+input (Env mBuf) str = atomically $ do+ res <- readTVar mBuf+ case res of+ Nothing -> writeTVar mBuf (Just str) >> return True+ Just _ -> return False++-- | Output the buffer contents.+output :: Env -> IO (Maybe String)+output (Env mBuf) = atomically $ do+ res <- readTVar mBuf+ writeTVar mBuf Nothing+ return res++------------------------------------------------------------------------++-- | Spec for echo.++prop_echoOK :: Env -> Property+prop_echoOK env = forAllCommands echoSM' Nothing $ \cmds -> monadicIO $ do+ (hist, _, res) <- runCommands echoSM' cmds+ prettyCommands echoSM' hist (res === Ok)+ where echoSM' = echoSM env++prop_echoParallelOK :: Bool -> Env -> Property+prop_echoParallelOK problem env = forAllParallelCommands echoSM' $ \cmds -> monadicIO $ do+ let n | problem = 2+ | otherwise = 1+ prettyParallelCommands cmds =<< runParallelCommandsNTimes n echoSM' cmds+ where echoSM' = echoSM env++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+ , invariant = Nothing+ , distribution = Nothing+ , shrinker = mShrinker+ , semantics = mSemantics+ , mock = mMock+ }+ 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++ -- | 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.+ mGenerator :: Model Symbolic -> Gen (Action Symbolic)+ mGenerator _ = oneof+ [ In <$> arbitrary+ , return Echo+ ]++ -- | Trivial shrinker.+ mShrinker :: Action Symbolic -> [Action Symbolic]+ mShrinker _ = []++ -- | 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?+ 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 instance ToExpr (Model Concrete)++-- | The model contains the last string that was communicated in an input+-- action.+data Model (r :: * -> *)+ = -- | The model hasn't been initialized.+ Empty+ | -- | Last input string (a buffer with size one).+ Buf String+ deriving (Eq, Show, Generic)++-- | Actions supported by the system.+data Action (r :: * -> *)+ = -- | Input a string, which should be echoed later.+ In String+ -- | Request a string output.+ | Echo+ deriving (Show, Generic1, Rank2.Foldable, Rank2.Traversable, Rank2.Functor)++-- | The system gives a single type of output response, containing a string+-- with the input previously received.+data Response (r :: * -> *)+ = -- | Input acknowledgment.+ InAck+ -- | The previous action wasn't an input, so there is no input to echo.+ -- This is: the buffer is empty.+ | ErrEmpty+ -- | There is already a string in the buffer.+ | ErrFull+ -- | Output string.+ | Out String+ deriving (Show, Generic1, Rank2.Foldable, Rank2.Traversable, Rank2.Functor)
test/MemoryReference.hs view
@@ -152,7 +152,7 @@ sm :: Bug -> StateMachine Model Command IO Response sm bug = StateMachine initModel transition precondition postcondition- Nothing Nothing generator Nothing shrinker (semantics bug) id mock+ Nothing generator Nothing shrinker (semantics bug) mock prop_sequential :: Bug -> Property prop_sequential bug = forAllCommands sm' Nothing $ \cmds -> monadicIO $ do
test/Spec.hs view
@@ -1,20 +1,33 @@ module Main (main) where import Prelude+import System.Exit+ (ExitCode(..))+import System.Process+ (rawSystem)+import Test.DocTest+ (doctest) import Test.Tasty+ (TestTree, defaultMain, testGroup, withResource)+import Test.Tasty.HUnit+ (testCase) import Test.Tasty.QuickCheck+ (expectFailure, ioProperty, testProperty,+ withMaxSuccess) import CircularBuffer import qualified CrudWebserverDb as WS import DieHard+import Echo import MemoryReference import TicketDispenser ------------------------------------------------------------------------ -tests :: TestTree-tests = testGroup "Tests"- [ testProperty "Die Hard"+tests :: Bool -> TestTree+tests docker0 = testGroup "Tests"+ [ testCase "Doctest Z module" (doctest ["src/Test/StateMachine/Z.hs"])+ , testProperty "Die Hard" (expectFailure (withMaxSuccess 1000 prop_dieHard)) , testGroup "Memory reference" [ testProperty "No bug" (prop_sequential None)@@ -23,10 +36,10 @@ , testProperty "Race bug parallel" (expectFailure (prop_parallel Race)) ] , testGroup "Crud webserver"- [ webServer WS.None 8800 "No bug" WS.prop_crudWebserverDb- , webServer WS.Logic 8801 "Logic bug" (expectFailure . WS.prop_crudWebserverDb)- , webServer WS.Race 8802 "No race bug" WS.prop_crudWebserverDb- , webServer WS.Race 8803 "Race bug" (expectFailure . WS.prop_crudWebserverDbParallel)+ [ webServer docker0 WS.None 8800 "No bug" WS.prop_crudWebserverDb+ , webServer docker0 WS.Logic 8801 "Logic bug" (expectFailure . WS.prop_crudWebserverDb)+ , webServer docker0 WS.Race 8802 "No race bug" WS.prop_crudWebserverDb+ , webServer docker0 WS.Race 8803 "Race bug" (expectFailure . WS.prop_crudWebserverDbParallel) ] , testGroup "Ticket dispenser" [ ticketDispenser "sequential" prop_ticketDispenser@@ -47,11 +60,18 @@ , testProperty "`prop_circularBuffer`: the fixed version is correct" prop_circularBuffer ]+ , testGroup "Echo"+ [ testProperty "sequential" (ioProperty (prop_echoOK <$> mkEnv))+ , testProperty "parallel ok" (ioProperty (prop_echoParallelOK False <$> mkEnv))+ , testProperty "parallel bad, see issue #218"+ (expectFailure (ioProperty (prop_echoParallelOK True <$> mkEnv)))+ ] ] where- webServer bug port test prop =- withResource (WS.setup bug WS.connectionString port) WS.cleanup- (const (testProperty test (prop port)))+ webServer docker bug port test prop+ | docker = withResource (WS.setup bug WS.connectionString port) WS.cleanup+ (const (testProperty test (prop port)))+ | otherwise = testCase ("No docker, skipping: " ++ test) (return ()) ticketDispenser test prop = withResource setupLock cleanupLock@@ -60,4 +80,10 @@ ------------------------------------------------------------------------ main :: IO ()-main = defaultMain tests+main = do+ -- Check if docker is avaiable.+ ec <- rawSystem "docker" ["version"]+ let docker = case ec of+ ExitSuccess -> True+ ExitFailure _ -> False+ defaultMain (tests docker)
test/TicketDispenser.hs view
@@ -15,7 +15,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) ----- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com> -- Stability : provisional -- Portability : non-portable (GHC extensions) --@@ -192,8 +192,7 @@ sm :: SharedExclusive -> DbLock -> StateMachine Model Action IO Response sm se files = StateMachine initModel transitions preconditions postconditions- Nothing Nothing generator Nothing- shrinker (semantics se files) id mock+ Nothing generator Nothing shrinker (semantics se files) mock -- Sequentially the model is consistent (even though the lock is -- shared).