diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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: diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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/); diff --git a/quickcheck-state-machine.cabal b/quickcheck-state-machine.cabal --- a/quickcheck-state-machine.cabal +++ b/quickcheck-state-machine.cabal @@ -1,6 +1,6 @@ cabal-version: >=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, diff --git a/src/Test/StateMachine.hs b/src/Test/StateMachine.hs --- a/src/Test/StateMachine.hs +++ b/src/Test/StateMachine.hs @@ -4,7 +4,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- Stability : provisional -- Portability : non-portable (GHC extensions) -- @@ -18,7 +18,6 @@ ( -- * Sequential property combinators forAllCommands , transitionMatrix - , modelCheck , runCommands , prettyCommands , checkCommandNames diff --git a/src/Test/StateMachine/Logic.hs b/src/Test/StateMachine/Logic.hs --- a/src/Test/StateMachine/Logic.hs +++ b/src/Test/StateMachine/Logic.hs @@ -7,7 +7,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- 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 diff --git a/src/Test/StateMachine/Parallel.hs b/src/Test/StateMachine/Parallel.hs --- a/src/Test/StateMachine/Parallel.hs +++ b/src/Test/StateMachine/Parallel.hs @@ -9,7 +9,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- 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 ------------------------------------------------------------------------ diff --git a/src/Test/StateMachine/Sequential.hs b/src/Test/StateMachine/Sequential.hs --- a/src/Test/StateMachine/Sequential.hs +++ b/src/Test/StateMachine/Sequential.hs @@ -12,7 +12,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- 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) diff --git a/src/Test/StateMachine/Types.hs b/src/Test/StateMachine/Types.hs --- a/src/Test/StateMachine/Types.hs +++ b/src/Test/StateMachine/Types.hs @@ -14,7 +14,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- 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) } diff --git a/src/Test/StateMachine/Types/Environment.hs b/src/Test/StateMachine/Types/Environment.hs --- a/src/Test/StateMachine/Types/Environment.hs +++ b/src/Test/StateMachine/Types/Environment.hs @@ -8,7 +8,7 @@ -- Copyright : (C) 2017, Jacob Stanley -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- Stability : provisional -- Portability : non-portable (GHC extensions) -- diff --git a/src/Test/StateMachine/Types/History.hs b/src/Test/StateMachine/Types/History.hs --- a/src/Test/StateMachine/Types/History.hs +++ b/src/Test/StateMachine/Types/History.hs @@ -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 +-- Maintainer : Stevan Andjelkovic -- 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) ------------------------------------------------------------------------ diff --git a/src/Test/StateMachine/Types/References.hs b/src/Test/StateMachine/Types/References.hs --- a/src/Test/StateMachine/Types/References.hs +++ b/src/Test/StateMachine/Types/References.hs @@ -11,7 +11,7 @@ -- Copyright : (C) 2017, Jacob Stanley -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- Stability : provisional -- Portability : non-portable (GHC extensions) -- diff --git a/src/Test/StateMachine/Utils.hs b/src/Test/StateMachine/Utils.hs --- a/src/Test/StateMachine/Utils.hs +++ b/src/Test/StateMachine/Utils.hs @@ -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 +-- Maintainer : Stevan Andjelkovic -- Stability : provisional -- Portability : non-portable (GHC extensions) -- diff --git a/src/Test/StateMachine/Z.hs b/src/Test/StateMachine/Z.hs --- a/src/Test/StateMachine/Z.hs +++ b/src/Test/StateMachine/Z.hs @@ -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 +-- Maintainer : Stevan Andjelkovic -- 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) diff --git a/test/CircularBuffer.hs b/test/CircularBuffer.hs --- a/test/CircularBuffer.hs +++ b/test/CircularBuffer.hs @@ -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 diff --git a/test/CrudWebserverDb.hs b/test/CrudWebserverDb.hs --- a/test/CrudWebserverDb.hs +++ b/test/CrudWebserverDb.hs @@ -25,7 +25,7 @@ -- (C) 2017-2018, Stevan Andjelkovic -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- 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 diff --git a/test/DieHard.hs b/test/DieHard.hs --- a/test/DieHard.hs +++ b/test/DieHard.hs @@ -13,7 +13,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- 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 diff --git a/test/Echo.hs b/test/Echo.hs new file mode 100644 --- /dev/null +++ b/test/Echo.hs @@ -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 +-- 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) diff --git a/test/MemoryReference.hs b/test/MemoryReference.hs --- a/test/MemoryReference.hs +++ b/test/MemoryReference.hs @@ -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 diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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) diff --git a/test/TicketDispenser.hs b/test/TicketDispenser.hs --- a/test/TicketDispenser.hs +++ b/test/TicketDispenser.hs @@ -15,7 +15,7 @@ -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- --- Maintainer : Stevan Andjelkovic +-- Maintainer : Stevan Andjelkovic -- 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).