diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +#### 0.0.0 + + * Initial release. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Stevan Andjelkovic, Daniel Gustafsson (c) 2017 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Stevan Andjelkovic nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,236 @@ +## quickcheck-state-machine + +[![Hackage](https://img.shields.io/hackage/v/quickcheck-state-machine.svg)](https://hackage.haskell.org/package/quickcheck-state-machine) +[![Build Status](https://api.travis-ci.org/advancedtelematic/quickcheck-state-machine.svg?branch=master)](https://travis-ci.org/advancedtelematic/quickcheck-state-machine) + +`quickcheck-state-machine` is a Haskell library, based +on [QuickCheck](https://hackage.haskell.org/package/QuickCheck), for testing +stateful programs. The library is different from +the +[`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html) approach +in that it lets the user specify the correctness by means of a state machine +based model using pre- and post-conditions. The advantage of the state machine +approach is twofold: 1) specifying the correctness of your programs becomes less +adhoc, and 2) you get testing for race conditions for free. + +The combination of state machine based model specification and property based +testing first appeard in Erlang's proprietary QuickCheck. The +`quickcheck-state-machine` library can be seen as an attempt to provide similar +functionality to Haskell's QuickCheck library. + +### Sample run (teaser) + +Here's a sample output from when we look for race conditions in the mutable +reference example: + +``` +> quickCheck (MutableReference.prop_parallel RaceCondition) +*** Failed! (after 5 tests and 6 shrinks): + +Couldn't linearise: + +┌──────────────────────┐ +│ New │ +│ ⟶ $0 │ +└──────────────────────┘ + │ ┌────────┐ + │ │ Inc $0 │ +┌─────────┐ │ │ │ +│ Inc $0 │ │ │ │ +│ │ │ │ ⟶ () │ +│ │ │ └────────┘ +│ ⟶ () │ │ +└─────────┘ │ +┌─────────┐ │ +│ Read $0 │ │ +│ ⟶ 1 │ │ +└─────────┘ │ + + +``` + +Clearly, if we increment a mutable reference in parallel we can end up with a +race condition. 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/example/src/MutableReference.hs). + +### How it works + +The rought idea is that the user of the library is asked to provide: + + * a datatype of commands; + * a datatype model; + * pre- and post-conditions of the commands on the model; + * a state transition function that given a model and a command advances the + model to its next state; + * a way to generate and shrink commands; + * semantics for executing the commands. + +The library then gives back a sequential and a parallel property. + +#### Sequential property + +The *sequential property* checks if the model is consistent with respect to the +semantics. The way this is done is: + + 1. generate a list of commands; + + 2. starting from the initial model, for each command do the the following: + + 1. check that the pre-condition holds; + 2. if so, execute the command using the semantics; + 3. check if the the post-condition holds; + 4. advance the model using the transition function. + + 3. If something goes wrong, shrink the initial list of commands and present a + minimal counter example. + +#### Parallel property + +The *parallel property* checks if parallel execution of the semantics can be +explained in terms of the sequential model. This is useful for trying to find +race conditions -- which normally can be tricky to test for. It works as +follows: + + 1. generate a list of commands that will act as a sequential prefix for the + parallel program (think of this as an initialisation bit that setups up + some state); + + 2. generate two lists of commands that will act as parallel suffixes; + + 3. execute the prefix sequentially; + + 4. execute the suffixes in parallel and gather the a trace (or history) of + invocations and responses of each command; + + 5. try to find a possible sequential interleaving of command invocations and + responses that respects the post-conditions. + +The last step basically tries to find +a [linearisation](https://en.wikipedia.org/wiki/Linearizability) of calls that +could have happend on a single thread. + +### Examples + +To get started it is perhaps easiest to have a look at one of the several +examples: + + * The water jug problem from *Die Hard 2* -- this is a + simple + [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/DieHard.hs) of + a specification where we use the sequential property to find a solution + (counter example) to a puzzle from an action movie. Note that this example + has no meaningful semantics, we merely model-check. It might be helpful to + compare the solution to the + Hedgehog + [solution](http://clrnd.com.ar/posts/2017-04-21-the-water-jug-problem-in-hedgehog.html) and + the + TLA+ + [solution](https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla); + + * The + union-find + [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/UnionFind.hs) -- + another use of the sequential property, this time with a useful semantics + (imperative implementation of the union-find algorithm). It could be useful + to compare the solution to the one that appears in the paper *Testing + Monadic Code with + QuickCheck* [[PS](http://www.cse.chalmers.se/~rjmh/Papers/QuickCheckST.ps)], + which is + the + [`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html) module + is based on; + + + * Mutable + reference + [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference.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 counter examples are + minimal, are specified in a + separate + [module](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference/Prop.hs); + + * Ticket + dispenser + [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/TicketDispenser.hs) -- + a simpler example where the parallel property is used once again to find a + race condition. This is an example used in the *Testing a Database for Race + Conditions with QuickCheck* and *Testing the Hard Stuff and Staying + Sane* + [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf), + [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)] papers. + +All examples have an associated `Spec` module located in +the +[`example/test`](https://github.com/advancedtelematic/quickcheck-state-machine/tree/master/example/test) directory. +These make use of the properties in the examples, and get tested as part +of +[Travis CI](https://travis-ci.org/advancedtelematic/quickcheck-state-machine). + +To get a better feel for the examples it might be helpful to `git clone` this +repo, `cd` into the `example/` directory and fire up `stack ghci` and run the +different properties interactively. + +### How to contribute + +The `quickcheck-state-machine` library is still very experimental. + +We would like to encourage users to try it out, and join the discussion of how +we can improve it on the issue tracker! + +### See also + + * The QuickCheck + bugtrack [issue](https://github.com/nick8325/quickcheck/issues/139) -- where + the initial discussion about how how to add state machine based testing to + QuickCheck started; + + * *Finding Race Conditions in Erlang with QuickCheck and + PULSE* + [[PDF](http://www.cse.chalmers.se/~nicsma/papers/finding-race-conditions.pdf), + [video](https://vimeo.com/6638041)] -- this is the first paper to describe + how Erlang's QuickCheck works (including the parallel testing); + + * *Linearizability: a correctness condition for concurrent + objects* [[PDF](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)], this + is a classic paper that describes the main technique of the parallel + property; + + * Aphyr's blogposts about [Jepsen](https://github.com/jepsen-io/jepsen), which + also uses the linearisability technique, and has found bugs in many + distributed systems: + + - [Knossos: Redis and linearizability](https://aphyr.com/posts/309-knossos-redis-and-linearizability) + - [Strong consistency models](https://aphyr.com/posts/313-strong-consistency-models) + - [Computational techniques in Knossos](https://aphyr.com/posts/314-computational-techniques-in-knossos) + - [Serializability, linearizability, and locality](https://aphyr.com/posts/333-serializability-linearizability-and-locality) + + * The use of state machines to model and verify properties about programs is + quite well-established, as witnessed by several books on the subject: + + - [Specifying Systems](https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/): + The TLA+ Language and Tools for Hardware and Software Engineers + - [Modeling in Event-B](http://www.event-b.org/abook.html): System and + Software Engineering + - [Abstract State Machines](http://www.di.unipi.it/~boerger/AsmBook/): A + Method for High-Level System Design and Analysis + + 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: + + - Lamport's + [*Computation and State Machines*](https://www.microsoft.com/en-us/research/publication/computation-state-machines/); + + - Gurevich's + [*Evolving Algebras 1993: Lipari Guide*](https://www.microsoft.com/en-us/research/publication/103-evolving-algebras-1993-lipari-guide/) and + *Sequential Abstract State Machines Capture Sequential + Algorithms* + [[PDF](http://delta-apache-vm.cs.tau.ac.il/~nachumd/models/gurevich.pdf)]. + +### License + +BSD-style (see the file LICENSE). diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/quickcheck-state-machine.cabal b/quickcheck-state-machine.cabal new file mode 100644 --- /dev/null +++ b/quickcheck-state-machine.cabal @@ -0,0 +1,63 @@ +name: quickcheck-state-machine +version: 0.0.0 +cabal-version: >=1.10 +build-type: Simple +license: BSD3 +license-file: LICENSE +copyright: Copyright (C) 2017, ATS Advanced Telematic Systems GmbH +maintainer: Stevan Andjelkovic +homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme +synopsis: Test monadic programs using state machine based models +description: + See README at +category: Testing +author: Stevan Andjelkovic +tested-with: GHC ==8.0.2 +extra-source-files: + README.md + CHANGELOG.md + +source-repository head + type: git + location: https://github.com/advancedtelematic/quickcheck-state-machine + +library + exposed-modules: + Test.StateMachine + Test.StateMachine.Internal.AlphaEquality + Test.StateMachine.Internal.IxMap + Test.StateMachine.Internal.Parallel + Test.StateMachine.Internal.ScopeCheck + Test.StateMachine.Internal.Sequential + Test.StateMachine.Internal.Types + Test.StateMachine.Internal.Types.IntRef + Test.StateMachine.Internal.Utils + Test.StateMachine.Internal.Utils.BoxDrawer + Test.StateMachine.Types + build-depends: + ansi-wl-pprint >=0.6.7.3 && <0.7, + base >=4.7 && <5, + constraints >=0.9.1 && <0.10, + containers >=0.5.7.1 && <0.6, + mtl >=2.2.1 && <2.3, + parallel-io >=0.3.3 && <0.4, + QuickCheck >=2.9.2 && <2.10, + random ==1.1.*, + singletons ==2.2.*, + stm >=2.4.4.1 && <2.5 + default-language: Haskell2010 + hs-source-dirs: src + +test-suite quickcheck-state-machine-test + type: exitcode-stdio-1.0 + main-is: Spec.hs + build-depends: + base >=4.9.1.0 && <4.10, + hspec >=2.4.3 && <2.5, + mtl >=2.2.1 && <2.3, + QuickCheck >=2.9.2 && <2.10, + quickcheck-state-machine >=0.0.0 && <0.1, + random ==1.1.* + default-language: Haskell2010 + hs-source-dirs: test + ghc-options: -threaded -rtsopts -with-rtsopts=-N diff --git a/src/Test/StateMachine.hs b/src/Test/StateMachine.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine.hs @@ -0,0 +1,119 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- The main module for state machine based testing. +-- +----------------------------------------------------------------------------- + +module Test.StateMachine + ( -- * Sequential property helper + sequentialProperty + , sequentialProperty' + -- * Parallel property helper + , parallelProperty + , parallelProperty' + , module Test.StateMachine.Types + ) where + +import Control.Monad.State + (StateT, evalStateT, lift, replicateM_) +import qualified Data.Map as M +import Test.QuickCheck + (Gen) +import Test.QuickCheck.Monadic + (monadic, monadicIO, run) +import Test.QuickCheck.Property + (Property, forAllShrink) + +import qualified Test.StateMachine.Internal.IxMap as IxM +import Test.StateMachine.Internal.Parallel +import Test.StateMachine.Internal.Sequential +import Test.StateMachine.Internal.Types +import Test.StateMachine.Internal.Utils +import Test.StateMachine.Types + +------------------------------------------------------------------------ + +-- | This function builds a property that tests if your model is agrees +-- with your semantics when running commands sequentially. +sequentialProperty + :: CommandConstraint ix cmd + => Monad m + => Show (model ConstIntRef) + => StateMachineModel model cmd -- ^ Model + -> Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator + -> (forall resp refs'. Shrinker (cmd refs' resp)) -- ^ Shrinker + -> (forall resp. cmd refs resp -> m (Response_ refs resp)) -- ^ Semantics + -> (m Property -> Property) + -> Property +sequentialProperty smm gen shrinker sem runM = + sequentialProperty' smm (lift gen) () shrinker (const (const sem)) runM + +-- | Same as above, except it provides more flexibility. +sequentialProperty' + :: CommandConstraint ix cmd + => Show (model ConstIntRef) + => Monad m + => StateMachineModel model cmd -- ^ Model + -> StateT s Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator + -> s -- ^ Generator state + -> (forall resp refs'. Shrinker (cmd refs' resp)) -- ^ Shrinker + -> (forall resp. model ConstIntRef -> + MayResponse_ ConstIntRef resp -> + cmd refs resp -> + m (Response_ refs resp)) -- ^ Semantics + -> (m Property -> Property) + -> Property +sequentialProperty' smm gen s shrinker sem runM = + forAllShrink + (fst . fst <$> liftGen' gen s 0 M.empty) + (liftShrink shrinker) + $ \cmds -> collectStats cmds $ + monadic (runM . flip evalStateT IxM.empty) $ + checkSequentialInvariant smm (initialModel smm) sem cmds + +------------------------------------------------------------------------ + +-- | This function builds a property that tests your semantics for race +-- conditions, by runnings commands in parallel and then trying to +-- linearise the resulting history. +-- +-- /Note:/ Make sure that your model passes the sequential property first. +parallelProperty + :: CommandConstraint ix cmd + => StateMachineModel model cmd -- ^ Model + -> Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator + -> (forall resp refs'. Shrinker (cmd refs' resp)) -- ^ Shrinker + -> (forall resp. cmd refs resp -> IO (Response_ refs resp)) -- ^ Semantics + -> Property +parallelProperty smm gen shrinker sem + = parallelProperty' smm (lift gen) () shrinker sem (return ()) + +parallelProperty' + :: CommandConstraint ix cmd + => StateMachineModel model cmd -- ^ Model + -> StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator + -> genState + -> (forall resp refs'. Shrinker (cmd refs' resp)) -- ^ Shrinker + -> (forall resp. cmd refs resp -> IO (Response_ refs resp)) -- ^ Semantics + -> IO () -- ^ Cleanup + -> Property +parallelProperty' smm gen genState shrinker sem clean + = forAllShrink + (liftGenFork' gen genState) + (liftShrinkFork shrinker) + $ \fork -> monadicIO $ replicateM_ 10 $ do + run clean + hist <- run $ liftSemFork sem fork + checkParallelInvariant smm hist diff --git a/src/Test/StateMachine/Internal/AlphaEquality.hs b/src/Test/StateMachine/Internal/AlphaEquality.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/AlphaEquality.hs @@ -0,0 +1,119 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.AlphaEquality +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module provides \(\alpha\)-equality for internal commands. This +-- functionality isn't used anywhere in the library, but can be useful +-- for writing +-- . +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.AlphaEquality + ( alphaEq + , alphaEqFork + ) where + +import Control.Monad + (forM) +import Control.Monad.State + (State, get, put, runState) +import Data.Kind + (Type) +import Data.Singletons.Decide + (SDecide) +import Data.Singletons.Prelude + (Proxy(..)) + +import Test.StateMachine.Internal.IxMap + (IxMap) +import qualified Test.StateMachine.Internal.IxMap as IxM +import Test.StateMachine.Internal.Types +import Test.StateMachine.Types + +------------------------------------------------------------------------ + +canonical' + :: forall (ix :: Type) (cmd :: Signature ix) + . SDecide ix + => IxTraversable cmd + => HasResponse cmd + => IxMap ix IntRef ConstIntRef + -> [IntRefed cmd] + -> ([IntRefed cmd], IxMap ix IntRef ConstIntRef) +canonical' im = flip runState im . go + where + go :: [IntRefed cmd] -> State (IxMap ix IntRef ConstIntRef) [IntRefed cmd] + go xs = forM xs $ \(IntRefed cmd ref) -> do + cmd' <- ifor (Proxy :: Proxy ConstIntRef) cmd $ \ix iref -> + (IxM.! (ix, iref)) <$> get + ref' <- case response cmd of + SResponse -> return () + SReference i -> do + m <- get + let ref' = IntRef (Ref $ IxM.size i m) (Pid 0) + put $ IxM.insert i ref ref' m + return ref' + return $ IntRefed cmd' ref' + +canonical + :: forall ix (cmd :: Signature ix) + . SDecide ix + => IxTraversable cmd + => HasResponse cmd + => [IntRefed cmd] + -> [IntRefed cmd] +canonical = fst . canonical' IxM.empty + +canonicalFork + :: forall ix (cmd :: Signature ix) + . SDecide ix + => IxTraversable cmd + => HasResponse cmd + => Fork [IntRefed cmd] + -> Fork [IntRefed cmd] +canonicalFork (Fork l p r) = Fork l' p' r' + where + (p', im') = canonical' IxM.empty p + l' = fst $ canonical' im' l + r' = fst $ canonical' im' r + +-- | Check if two lists of commands are equal modulo +-- \(\alpha\)-conversion. +alphaEq + :: forall ix (cmd :: Signature ix) + . SDecide ix + => IxTraversable cmd + => HasResponse cmd + => Eq (IntRefed cmd) + => [IntRefed cmd] -- ^ The two + -> [IntRefed cmd] -- ^ input lists. + -> Bool +alphaEq c0 c1 = canonical c0 == canonical c1 + +-- | Check if two forks of commands are equal modulo +-- \(\alpha\)-conversion. +alphaEqFork + :: forall ix (cmd :: Signature ix) + . SDecide ix + => IxTraversable cmd + => HasResponse cmd + => Eq (IntRefed cmd) + => Fork [IntRefed cmd] -- ^ The two + -> Fork [IntRefed cmd] -- ^ input forks. + -> Bool +alphaEqFork f1 f2 = canonicalFork f1 == canonicalFork f2 diff --git a/src/Test/StateMachine/Internal/IxMap.hs b/src/Test/StateMachine/Internal/IxMap.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/IxMap.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.IxMap +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module provides indexed maps. These are used to implement support for +-- multiple references. +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.IxMap + ( IxMap + , empty + , (!) + , lookup + , member + , insert + , size + ) where + +import Data.Kind + (Type) +import Data.Map + (Map) +import qualified Data.Map as M +import Data.Proxy + (Proxy(Proxy)) +import Data.Singletons.Decide + ((:~:)(Refl), Decision(Proved), SDecide, (%~)) +import Data.Singletons.Prelude + (type (@@), Sing, TyFun) +import Prelude hiding + (lookup) + +------------------------------------------------------------------------ + +-- | An 'ix'-indexed family of maps. +newtype IxMap (ix :: Type) (k :: Type) (vs :: TyFun ix Type -> Type) + = IxMap (forall i. Proxy vs -> Sing (i :: ix) -> Map k (vs @@ i)) + +-- | The empty map. +empty :: IxMap i k vs +empty = IxMap (\_ _ -> M.empty) + +-- | Partial lookup function. +(!) :: Ord k => IxMap ix k vs -> (Sing i, k) -> vs @@ i +IxMap m ! (i, k) = m Proxy i M.! k + +-- | Total version of the above. +lookup :: Ord k => Sing i -> k -> IxMap ix k vs -> Maybe (vs @@ i) +lookup i k (IxMap m) = M.lookup k (m Proxy i) + +-- | Key membership check. +member :: Ord k => Sing (i :: ix) -> k -> IxMap ix k vs -> Bool +member i k (IxMap m) = M.member k (m Proxy i) + +-- | Map insertion. +insert + :: (Ord k, SDecide ix) + => Sing i -> k -> vs @@ i -> IxMap ix k vs -> IxMap ix k vs +insert i k v (IxMap m) = IxMap $ \_ j -> case i %~ j of + Proved Refl -> M.insert k v (m Proxy i) + _ -> m Proxy j + +-- | Size of the key set. +size :: Sing (i :: ix) -> IxMap ix k vs -> Int +size i (IxMap m) = M.size (m Proxy i) diff --git a/src/Test/StateMachine/Internal/Parallel.hs b/src/Test/StateMachine/Internal/Parallel.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/Parallel.hs @@ -0,0 +1,347 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.Parallel +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module contains the building blocks needed to implement the +-- 'Test.StateMachine.parallelProperty' helper. +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.Parallel + ( liftGenFork + , liftGenFork' + , liftShrinkFork + , liftSemFork + , checkParallelInvariant + ) where + +import Control.Concurrent + (threadDelay) +import Control.Concurrent.ParallelIO.Local + (parallel_, withPool) +import Control.Concurrent.STM + (STM, atomically) +import Control.Concurrent.STM.TChan + (TChan, newTChanIO, tryReadTChan, writeTChan) +import Control.Monad + (foldM) +import Control.Monad.State + (StateT, evalStateT, execStateT, lift) +import Data.Dynamic + (Dynamic, fromDynamic, toDyn) +import Data.Kind + (Type) +import Data.List + (partition) +import qualified Data.Map as M +import Data.Maybe + (fromMaybe) +import Data.Singletons.Decide + (SDecide) +import Data.Singletons.Prelude + (DemoteRep, SingKind, TyFun, fromSing) +import Data.Tree + (Tree(Node)) +import Data.Typeable + (Typeable) +import System.Random + (randomRIO) +import Test.QuickCheck + (Gen, Property, counterexample, property, (.&&.)) +import Test.QuickCheck.Monadic + (PropertyM) +import Text.PrettyPrint.ANSI.Leijen + (Doc, Pretty, pretty, prettyList, text, vsep, (<+>)) + +import Test.StateMachine.Internal.IxMap + (IxMap) +import qualified Test.StateMachine.Internal.IxMap as IxM +import Test.StateMachine.Internal.Sequential +import Test.StateMachine.Internal.Types +import Test.StateMachine.Internal.Types.IntRef + (showRef) +import Test.StateMachine.Internal.Utils +import Test.StateMachine.Internal.Utils.BoxDrawer +import Test.StateMachine.Types + +------------------------------------------------------------------------ + +-- | Lift a generator of untyped commands with reference placeholders +-- into a generator of forks of untyped internal commands. +liftGenFork + :: Ord ix + => SingKind ix + => DemoteRep ix ~ ix + => IxTraversable cmd + => HasResponse cmd + => Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator to be lifted. + -> Gen (Fork [IntRefed cmd]) +liftGenFork gen = liftGenFork' (lift gen) () + +liftGenFork' + :: Ord ix + => SingKind ix + => DemoteRep ix ~ ix + => IxTraversable cmd + => HasResponse cmd + => StateT genState Gen (Untyped cmd (RefPlaceholder ix)) + -> genState + -> Gen (Fork [IntRefed cmd]) +liftGenFork' gen gs = do + ((prefix, gs'), ns) <- liftGen' gen gs 0 M.empty + left <- fst . fst <$> liftGen' gen gs' 1 ns + right <- fst . fst <$> liftGen' gen gs' 2 ns + return $ Fork + (map (\(IntRefed cmd miref) -> + IntRefed (ifmap (fixPid ns) cmd) miref) left) + prefix + (map (\(IntRefed cmd miref) -> + IntRefed (ifmap (fixPid ns) cmd) miref) right) + where + fixPid ns i iref@(IntRef (Ref ref) _) + | ref <= ns M.! fromSing i = IntRef (Ref ref) 0 + | otherwise = iref + +------------------------------------------------------------------------ + +-- | Lift a shrinker of internal commands into a shrinker of forks of +-- untyped internal commands. +liftShrinkFork + :: forall cmd + . IxFoldable cmd + => HasResponse cmd + => (forall resp. Shrinker (cmd ConstIntRef resp)) -- ^ Shrinker to be lifted. + -> Shrinker (Fork [IntRefed cmd]) +liftShrinkFork shrinker f@(Fork l0 p0 r0) = + + -- Only shrink the branches: + [ Fork l' p0 r' + | (l', r') <- shrinkPair (liftShrink shrinker) + (liftShrink shrinker) + (l0, r0) + ] ++ + + -- Only shrink the prefix: + shrinkPrefix f + + where + shrinkPrefix :: Fork [IntRefed cmd] -> [Fork [IntRefed cmd]] + shrinkPrefix (Fork _ [] _) = [] + shrinkPrefix (Fork l (p : ps) r) = + [ Fork l' [] r' ] ++ + [ Fork l'' (removeCommands p ps) r'' ] ++ + [ Fork l''' (p' : ps') r''' + | (p', Fork l''' ps' r''') <- shrinkPair (liftShrinker shrinker) + shrinkPrefix + (p, Fork l ps r) + ] + where + l' = removeManyCommands (p : ps) l + r' = removeManyCommands (p : ps) r + + l'' = removeCommands p l + r'' = removeCommands p r + + removeManyCommands :: [IntRefed cmd] -> [IntRefed cmd] -> [IntRefed cmd] + removeManyCommands [] ds = ds + removeManyCommands (c : cs) ds = removeManyCommands cs (removeCommands c ds) + +------------------------------------------------------------------------ + +type History cmd = [HistoryEvent (IntRefed cmd)] + +data HistoryEvent cmd + = InvocationEvent cmd Pid + | ResponseEvent Dynamic Pid + +getProcessIdEvent :: HistoryEvent cmd -> Pid +getProcessIdEvent (InvocationEvent _ pid) = pid +getProcessIdEvent (ResponseEvent _ pid) = pid + +data Operation cmd = forall resp. + (Show (GetResponse_ resp), + HasResponse cmd, + Typeable resp, + Typeable (Response_ ConstIntRef resp)) => + Operation (cmd ConstIntRef resp) (Response_ ConstIntRef resp) Pid + +instance (ShowCmd cmd, IxFunctor cmd) => Pretty (Operation cmd) where + pretty (Operation cmd resp _) = + text (showCmd $ ifmap (const showRef) cmd) <+> text "-->" <+> text (showResponse_ (response cmd) resp) + prettyList = vsep . map pretty + +takeInvocations :: History cmd -> [HistoryEvent (IntRefed cmd)] +takeInvocations = takeWhile $ \h -> case h of + InvocationEvent _ _ -> True + _ -> False + +findCorrespondingResp :: Pid -> History cmd -> [(Dynamic, History cmd)] +findCorrespondingResp _ [] = [] +findCorrespondingResp pid (ResponseEvent resp pid' : es) | pid == pid' = [(resp, es)] +findCorrespondingResp pid (e : es) = + [ (resp, e : es') | (resp, es') <- findCorrespondingResp pid es ] + +linearTree :: HasResponse cmd => History cmd -> [Tree (Operation cmd)] +linearTree [] = [] +linearTree es = + [ Node (Operation cmd (dynResp resp) pid) (linearTree es') + | InvocationEvent (IntRefed cmd _) pid <- takeInvocations es + , (resp, es') <- findCorrespondingResp pid $ filter1 (not . matchInv pid) es + ] + where + dynResp resp = fromMaybe (error "linearTree: impossible.") (fromDynamic resp) + + filter1 :: (a -> Bool) -> [a] -> [a] + filter1 _ [] = [] + filter1 p (x : xs) | p x = x : filter1 p xs + | otherwise = xs + + -- Hmm, is this enough? + matchInv pid (InvocationEvent _ pid') = pid == pid' + matchInv _ _ = False + +linearise + :: forall cmd model + . HasResponse cmd + => StateMachineModel model cmd + -> History cmd + -> Property +linearise _ [] = property True +linearise StateMachineModel {..} xs0 = anyP (step initialModel) . linearTree $ xs0 + where + step :: model ConstIntRef -> Tree (Operation cmd) -> Property + step m (Node (Operation cmd resp _) roses) = + postcondition m cmd resp .&&. + anyP' (step (transition m cmd resp)) roses + where + anyP' :: (a -> Property) -> [a] -> Property + anyP' _ [] = property True + anyP' p xs = anyP p xs + +------------------------------------------------------------------------ + +toForkOfOps :: forall cmd. HasResponse cmd => History cmd -> Fork [Operation cmd] +toForkOfOps h = Fork (mkOps l) p' (mkOps r) + where + (p, h') = partition (\e -> getProcessIdEvent e == 0) h + (l, r) = partition (\e -> getProcessIdEvent e == 1) h' + + p' = mkOps p + + mkOps :: [HistoryEvent (IntRefed cmd)] -> [Operation cmd] + mkOps [] = [] + mkOps (InvocationEvent (IntRefed cmd _) _ : ResponseEvent resp pid : es) + = Operation cmd (dynResp resp) pid : mkOps es + where + dynResp = fromMaybe (error "toForkOfOps: impossible.") . fromDynamic + mkOps _ = error "mkOps: Impossible." + +toBoxDrawings :: forall cmd. (IxFunctor cmd, ShowCmd cmd, HasResponse cmd) => History cmd -> Doc +toBoxDrawings h = exec evT (fmap out (toForkOfOps h)) + where + out :: [Operation cmd] -> [String] + out [] = [] + out (Operation cmd resp _ : os) = showCmd (ifmap (const showRef) cmd) + : showResponse_ (response cmd) resp + : out os + toEventType :: History cmd -> [(EventType, Pid)] + toEventType = map $ \e -> case e of + InvocationEvent _ pid -> (Open, pid) + ResponseEvent _ pid -> (Close, pid) + evT :: [(EventType, Pid)] + evT = toEventType (filter (\e -> getProcessIdEvent e `elem` [1,2]) h) + +------------------------------------------------------------------------ + +data HistoryKit cmd refs = HistoryKit + { getHistoryChannel :: TChan (HistoryEvent (IntRefed cmd)) + , getProcessIdHistory :: Pid + } + +mkHistoryKit :: Pid -> IO (HistoryKit cmd refs) +mkHistoryKit pid = do + chan <- newTChanIO + return $ HistoryKit chan pid + +runMany + :: SDecide ix + => IxFunctor cmd + => HasResponse cmd + => HistoryKit cmd ConstIntRef + -> (forall resp. cmd refs resp -> IO (Response_ refs resp)) + -> [IntRefed cmd] + -> StateT (IxMap ix IntRef refs) IO () +runMany kit sem = flip foldM () $ \_ cmd'@(IntRefed cmd iref) -> do + lift $ atomically $ writeTChan (getHistoryChannel kit) $ + InvocationEvent cmd' (getProcessIdHistory kit) + resp <- liftSem sem cmd iref + + lift $ do + threadDelay =<< randomRIO (0, 20) + atomically $ writeTChan (getHistoryChannel kit) $ + ResponseEvent (toDyn resp) (getProcessIdHistory kit) + +-- | Lift the semantics of a single typed command into a semantics for +-- forks of untyped internal commands. The prefix of the fork is +-- executed sequentially, while the two suffixes are executed in +-- parallel, and the result (or trace) is collected in a so called +-- history. +liftSemFork + :: forall + (ix :: Type) + (cmd :: Signature ix) + (refs :: TyFun ix Type -> Type) + . SDecide ix + => IxFunctor cmd + => HasResponse cmd + => (forall resp. cmd refs resp -> + IO (Response_ refs resp)) -- ^ Semantics to be lifted. + -> Fork [IntRefed cmd] + -> IO (History cmd) +liftSemFork sem (Fork left prefix right) = do + kit <- mkHistoryKit 0 + env <- execStateT (runMany kit sem prefix) IxM.empty + withPool 2 $ \pool -> + parallel_ pool + [ evalStateT (runMany (kit { getProcessIdHistory = 1}) sem left) env + , evalStateT (runMany (kit { getProcessIdHistory = 2}) sem right) env + ] + getChanContents $ getHistoryChannel kit + where + getChanContents :: forall a. TChan a -> IO [a] + getChanContents chan = reverse <$> atomically (go []) + where + go :: [a] -> STM [a] + go acc = do + mx <- tryReadTChan chan + case mx of + Just x -> go $ x : acc + Nothing -> return acc + +-- | Check if a history can be linearised. +checkParallelInvariant + :: (ShowCmd cmd, IxFunctor cmd, HasResponse cmd) + => StateMachineModel model cmd -> History cmd -> PropertyM IO () +checkParallelInvariant smm hist + = liftProperty + . counterexample (("Couldn't linearise:\n\n" ++) $ show $ toBoxDrawings hist) + $ linearise smm hist diff --git a/src/Test/StateMachine/Internal/ScopeCheck.hs b/src/Test/StateMachine/Internal/ScopeCheck.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/ScopeCheck.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.ScopeCheck +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module provides scope-checking for internal commands. This +-- functionality isn't used anywhere in the library, but can be useful +-- for writing +-- . +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.ScopeCheck + ( scopeCheck + , scopeCheckFork + ) where + +import Test.StateMachine.Internal.Types +import Test.StateMachine.Types + +------------------------------------------------------------------------ + +-- | Scope-check a list of untyped internal commands, i.e. make sure +-- that no command uses a reference that doesn't exist. +scopeCheck + :: forall cmd. (IxFoldable cmd, HasResponse cmd) + => [IntRefed cmd] -> Bool +scopeCheck = go [] + where + go :: [IntRef] -> [IntRefed cmd] -> Bool + go _ [] = True + go refs (IntRefed c miref : cs) = case response c of + SReference _ -> + all (\(Ex _ ref) -> ref `elem` refs) (itoList c) && + go (miref : refs) cs + SResponse -> + all (\(Ex _ ref) -> ref `elem` refs) (itoList c) && + go refs cs + +-- | Same as above, but for forks rather than lists. +scopeCheckFork + :: (IxFoldable cmd, HasResponse cmd) + => Fork [IntRefed cmd] -> Bool +scopeCheckFork (Fork l p r) = + scopeCheck (p ++ l) && + scopeCheck (p ++ r) diff --git a/src/Test/StateMachine/Internal/Sequential.hs b/src/Test/StateMachine/Internal/Sequential.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/Sequential.hs @@ -0,0 +1,265 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.Sequential +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module contains the building blocks needed to implement the +-- 'Test.StateMachine.sequentialProperty' helper. +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.Sequential + ( liftGen + , liftGen' + , liftShrinker + , liftShrink + , liftSem + , removeCommands + , collectStats + , checkSequentialInvariant + ) where + +import Control.Monad.State + (StateT, get, lift, mapStateT, modify, runStateT) +import Data.Functor.Compose + (Compose(..), getCompose) +import Data.Map + (Map) +import qualified Data.Map as M +import Data.Set + (Set) +import qualified Data.Set as S +import Data.Singletons.Decide + (SDecide) +import Data.Singletons.Prelude + (type (@@), DemoteRep, Proxy(Proxy), Sing, SingKind, + fromSing) +import Test.QuickCheck + (Gen, choose, classify, counterexample, label, + sized) +import Test.QuickCheck.Monadic + (PropertyM, monitor, pre, run) +import Test.QuickCheck.Property + (Property) + +import Test.StateMachine.Internal.IxMap + (IxMap) +import qualified Test.StateMachine.Internal.IxMap as IxM +import Test.StateMachine.Internal.Types +import Test.StateMachine.Internal.Types.IntRef + (showRef) +import Test.StateMachine.Internal.Utils +import Test.StateMachine.Types + +------------------------------------------------------------------------ + +-- | Lift a generator of untyped commands with reference placeholders +-- into a generator of lists of untyped internal commands. +liftGen + :: forall ix cmd + . Ord ix + => SingKind ix + => DemoteRep ix ~ ix + => IxTraversable cmd + => HasResponse cmd + => Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator to be lifted. + -> Pid -- ^ Process id. + -> Map ix Int -- ^ Keeps track of how many + -- refereces of sort 'ix' are in + -- scope. + -> Gen ([IntRefed cmd], Map ix Int) +liftGen gen pid + = fmap (\((rs, _), ns) -> (rs, ns)) + . liftGen' (lift gen) () pid + +-- | Same as the above, but for stateful generators. +liftGen' + :: forall ix cmd genState + . Ord ix + => SingKind ix + => DemoteRep ix ~ ix + => IxTraversable cmd + => HasResponse cmd + => StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Stateful + -- generator to be + -- lifted. + + -> genState -- ^ Initial + -- generator state. + -> Pid + -> Map ix Int + -> Gen (([IntRefed cmd], genState), Map ix Int) +liftGen' gen gs pid ns = sized $ \sz -> runStateT (runStateT (go sz) gs) ns + where + + go :: Int -> StateT genState (StateT (Map ix Int) Gen) [IntRefed cmd] + go 0 = return [] + go sz = do + + scopes <- lift get + + Untyped cmd <- genFromMaybe $ do + Untyped cmd <- mapStateT lift gen + cmd' <- lift $ lift $ getCompose $ ifor + (Proxy :: Proxy ConstIntRef) cmd (translate scopes) + return $ Untyped <$> cmd' + + ixref <- case response cmd of + SResponse -> return () + SReference i -> do + lift $ modify (M.insertWith (\_ old -> old + 1) (fromSing i) 0) + m <- lift get + return $ IntRef (Ref (m M.! fromSing i)) pid + + (IntRefed cmd ixref :) <$> go (sz - 1) + + translate + :: forall (i :: ix) + . Map ix Int + -> Sing i + -> RefPlaceholder ix @@ i + -> Compose Gen Maybe IntRef + translate scopes i _ = Compose $ case M.lookup (fromSing i) scopes of + Nothing -> return Nothing + Just u -> do + v <- choose (0, max 0 (u - 1)) + return . Just $ IntRef (Ref v) pid + +------------------------------------------------------------------------ + +-- | A shrinker of typed commands can be lifted to a shrinker of untyped +-- commands. +liftShrinker :: (forall resp. Shrinker (cmd ConstIntRef resp)) -> Shrinker (IntRefed cmd) +liftShrinker shrinker (IntRefed cmd miref) = + [ IntRefed cmd' miref + | cmd' <- shrinker cmd + ] + +-- | Lift a shrinker of internal commands into a shrinker of lists of +-- untyped internal commands. +liftShrink + :: IxFoldable cmd + => HasResponse cmd + => (forall resp. Shrinker (cmd ConstIntRef resp)) -- ^ Shrinker to be lifted. + -> Shrinker [IntRefed cmd] +liftShrink shrinker = go + where + go [] = [] + go (c : cs) = + [ [] ] ++ + [ removeCommands c cs ] ++ + [ c' : cs' | (c', cs') <- shrinkPair (liftShrinker shrinker) go (c, cs) ] + +-- | Remove commands that uses a reference. +removeCommands + :: forall cmd + . IxFoldable cmd + => HasResponse cmd + => IntRefed cmd -- ^ If this command returns a reference, then + -> [IntRefed cmd] -- ^ remove all commands that use that reference in + -- this list. If a command we remove uses another + -- reference, then we proceed recursively. + -> [IntRefed cmd] +removeCommands (IntRefed cmd0 miref0) cmds0 = + case response cmd0 of + SResponse -> cmds0 + SReference _ -> go cmds0 (S.singleton miref0) + where + go :: [IntRefed cmd] -> Set IntRef -> [IntRefed cmd] + go [] _ = [] + go (cmd@(IntRefed cmd' miref) : cmds) removed = + case response cmd' of + SReference _ | cmd' `uses` removed -> go cmds (S.insert miref removed) + | otherwise -> cmd : go cmds removed + SResponse | cmd' `uses` removed -> go cmds removed + | otherwise -> cmd : go cmds removed + +uses :: IxFoldable cmd => cmd ConstIntRef resp -> Set IntRef -> Bool +uses cmd xs = iany (\_ iref -> iref `S.member` xs) cmd + +------------------------------------------------------------------------ + +-- | Lift semantics of typed commands with external references, into +-- semantics for typed commands with internal references. +liftSem + :: forall ix cmd refs resp m + . SDecide ix + => Monad m + => IxFunctor cmd + => HasResponse cmd + => (cmd refs resp -> m (Response_ refs resp)) -- ^ Semantics to be lifted. + -> cmd ConstIntRef resp + -> MayResponse_ ConstIntRef resp + -> StateT (IxMap ix IntRef refs) m (Response_ ConstIntRef resp) +liftSem sem cmd iref = do + + env <- get + let cmd' = ifmap @_ @_ @_ @_ @refs (\s i -> env IxM.! (s, i)) cmd + + case response cmd' of + SResponse -> lift $ sem cmd' + SReference i -> do + ref <- lift $ sem cmd' + modify $ IxM.insert i iref ref + return iref + +------------------------------------------------------------------------ + +-- | Collects length statistics about the input list. +collectStats :: [a] -> Property -> Property +collectStats cmds + = classify (len == 0) "0 commands" + . classify (len >= 1 && len < 15) "1-15 commands" + . classify (len >= 15 && len < 30) "15-30 commands" + . classify (len >= 30) "30+ commands" + where + len = length cmds + +------------------------------------------------------------------------ + +-- | Check that the pre- and post-conditions hold in a sequential way. +checkSequentialInvariant + :: ShowCmd cmd + => Monad m + => SDecide ix + => IxFunctor cmd + => Show (model ConstIntRef) + => HasResponse cmd + => StateMachineModel model cmd + -> model ConstIntRef + -> (forall resp. model ConstIntRef -> MayResponse_ ConstIntRef resp -> cmd refs resp -> + m (Response_ refs resp)) + -> [IntRefed cmd] -- ^ List of commands to check. + -> PropertyM (StateT (IxMap ix IntRef refs) m) () +checkSequentialInvariant _ _ _ [] = return () +checkSequentialInvariant + smm@StateMachineModel {..} m sem (IntRefed cmd miref : cmds) = do + let s = takeWhile (/= ' ') $ showCmd $ ifmap (const showRef) cmd + monitor $ label s + pre $ precondition m cmd + resp <- run $ liftSem (sem m miref) cmd miref + let m' = transition m cmd resp + liftProperty $ + counterexample + ("\nThe model when the post-condition for `" ++ s ++ + "' fails is:\n\n " ++ show m ++ "\n\n" ++ + "The model transitions into:\n\n " ++ show m' + ) $ postcondition m cmd resp + checkSequentialInvariant smm m' sem cmds diff --git a/src/Test/StateMachine/Internal/Types.hs b/src/Test/StateMachine/Internal/Types.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/Types.hs @@ -0,0 +1,94 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.Types +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module exports some types that are used internally by the library. +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.Types + ( IntRef(..) + , Pid(..) + , Ref(..) + , ConstIntRef + , IntRefed(..) + , Fork(..) + , showResponse_ + , MayResponse_ + ) where + +import Data.Kind + (Type) +import Data.Monoid + ((<>)) +import Data.Singletons.Prelude + (type (@@), TyFun) +import Data.Typeable + (Typeable) +import Text.PrettyPrint.ANSI.Leijen + (Pretty, align, dot, indent, int, pretty, text, + underline, vsep, (<+>)) + +import Test.StateMachine.Internal.Types.IntRef +import Test.StateMachine.Types + +------------------------------------------------------------------------ + +-- | Type-level function that maybe returns a reference. +type family MayResponse_ (refs :: TyFun ix k -> Type) (resp :: Response ix) :: k where + MayResponse_ refs ('Response t) = () + MayResponse_ refs ('Reference i) = refs @@ i + +-- | Internal untyped commands. +data IntRefed (f :: Signature ix) where + IntRefed :: ( Show (GetResponse_ resp) + , Typeable (Response_ ConstIntRef resp) + , Typeable resp + ) => f ConstIntRef resp -> MayResponse_ ConstIntRef resp -> IntRefed f + +instance (IxFunctor cmd, ShowCmd cmd, HasResponse cmd) => Show (IntRefed cmd) where + show (IntRefed cmd miref) = showCmd (ifmap (\ _ r -> "(" ++ show r ++ ")") cmd) ++ " " ++ + case response cmd of + SResponse -> "()" + SReference _ -> "(" ++ show miref ++ ")" + +-- | Forks are used to represent parallel programs. They have a sequential +-- prefix (the middle argument of the constructor), and two parallel suffixes +-- (the left- and right-most argument of the constructor). +data Fork a = Fork a a a + deriving (Eq, Functor, Show, Ord, Read) + +instance Pretty a => Pretty (Fork a) where + pretty (Fork l p r) = vsep + [ underline $ text "Prefix:" + , indent 5 $ pretty p + , underline $ text "Parallel:" + , indent 2 $ int 1 <> dot <+> align (pretty l) + , indent 2 $ int 2 <> dot <+> align (pretty r) + ] + +------------------------------------------------------------------------ + +-- | Show function for 'Response_'. +showResponse_ + :: Show (GetResponse_ resp) + => SResponse ix resp -> Response_ ConstIntRef resp -> String +showResponse_ SResponse = show +showResponse_ (SReference _) = showRef diff --git a/src/Test/StateMachine/Internal/Types/IntRef.hs b/src/Test/StateMachine/Internal/Types/IntRef.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/Types/IntRef.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PolyKinds #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.Types +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module provides internal refereces. +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.Types.IntRef + ( IntRef(..) + , Pid(..) + , Ref(..) + , ConstIntRef + , showRef + ) where + +import Data.Singletons.Prelude + (ConstSym1) + +------------------------------------------------------------------------ + +-- | An internal (or integer) reference consists of a reference and a +-- process id. +data IntRef = IntRef Ref Pid + deriving (Eq, Ord, Show, Read) + +-- | A process id is merely a natural number that keeps track of which +-- thread the reference comes from. In the sequential case the process +-- id is always @0@. Likewise the sequential prefix of a parallel +-- program also has process id @0@, while the left suffix has process +-- id @1@, and then right suffix has process id @2@. +newtype Pid = Pid Int + deriving (Eq, Ord, Show, Read, Num) + +-- | A reference is natural number. +newtype Ref = Ref Int + deriving (Eq, Ord, Show, Read, Num) + +-- | Type-level function that constantly returns an internal reference. +type ConstIntRef = ConstSym1 IntRef + +showRef :: IntRef -> String +showRef (IntRef (Ref ref) (Pid pid)) = case pid of + 0 -> '$':show ref + _ -> '$':show ref ++ "::" ++ show pid diff --git a/src/Test/StateMachine/Internal/Utils.hs b/src/Test/StateMachine/Internal/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/Utils.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.Utils +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module exports some QuickCheck utility functions. Some of these should +-- perhaps be upstreamed. +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.Utils + ( Shrinker + , genFromMaybe + , anyP + , liftProperty + , shrinkPropertyHelper + , shrinkPropertyHelper' + , shrinkPair + ) where + +import Control.Monad.State + (StateT) +import Test.QuickCheck + (Gen, Property, Result(Failure), chatty, + counterexample, output, property, + quickCheckWithResult, stdArgs) +import Test.QuickCheck.Monadic + (PropertyM(MkPropertyM), monadicIO, run) +import Test.QuickCheck.Property + ((.&&.), (.||.)) + +------------------------------------------------------------------------ + +-- | The type of a shrinker function. +type Shrinker a = a -> [a] + +-- | Keep generating until we actually get a value. +genFromMaybe :: StateT s (StateT t Gen) (Maybe a) -> StateT s (StateT t Gen) a +genFromMaybe g = do + mx <- g + case mx of + Nothing -> genFromMaybe g + Just x -> return x + +-- | Lifts 'Prelude.any' to properties. +anyP :: (a -> Property) -> [a] -> Property +anyP p = foldr (\x ih -> p x .||. ih) (property False) + +-- | Lifts a plain property into a monadic property. +liftProperty :: Monad m => Property -> PropertyM m () +liftProperty prop = MkPropertyM (\k -> fmap (prop .&&.) <$> k ()) + +-- | Write a metaproperty on the output of QuickChecking a property using a +-- boolean predicate on the output. +shrinkPropertyHelper :: Property -> (String -> Bool) -> Property +shrinkPropertyHelper prop p = shrinkPropertyHelper' prop (property . p) + +-- | Same as above, but using a property predicate. +shrinkPropertyHelper' :: Property -> (String -> Property) -> Property +shrinkPropertyHelper' prop p = monadicIO $ do + result <- run $ quickCheckWithResult (stdArgs {chatty = False}) prop + case result of + Failure { output = outputLines } -> liftProperty $ + counterexample ("failed: " ++ outputLines) $ p outputLines + _ -> return () + +-- | Given shrinkers for the components of a pair we can shrink the pair. +shrinkPair :: Shrinker a -> Shrinker b -> Shrinker (a, b) +shrinkPair shrinkerA shrinkerB (x, y) = + [ (x', y) | x' <- shrinkerA x ] ++ + [ (x, y') | y' <- shrinkerB y ] diff --git a/src/Test/StateMachine/Internal/Utils/BoxDrawer.hs b/src/Test/StateMachine/Internal/Utils/BoxDrawer.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Internal/Utils/BoxDrawer.hs @@ -0,0 +1,97 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Internal.Parallel +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Mats Daniel Gustafsson +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module contains functions for drawing the history for the +-- 'Test.StateMachine.parallelProperty'. +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Internal.Utils.BoxDrawer + ( EventType(..) + , exec) + where + +import Text.PrettyPrint.ANSI.Leijen + (Doc, text, vsep) + +import Test.StateMachine.Internal.Types + (Fork(Fork)) +import Test.StateMachine.Internal.Types.IntRef + (Pid(..)) + +data EventType = Open | Close + deriving (Show) + +data Event = Event EventType Pid String + +data Cmd = Top | Start String | Active | Deactive | Ret String | Bottom + +compile :: [Event] -> ([Cmd], [Cmd]) +compile = go (Deactive, Deactive) + where + infixr 9 `add` + add :: (a,b) -> ([a], [b]) -> ([a], [b]) + add (x,y) (xs, ys) = (x:xs, y:ys) + + set :: (a, a) -> Pid -> a -> (a, a) + set (_x, y) (Pid 1) x' = (x', y) + set (x, _y) (Pid 2) y' = (x, y') + set _ pid _ = error $ "compile.set: unknown pid " ++ show pid + + go :: (Cmd, Cmd) -> [Event] -> ([Cmd], [Cmd]) + go _ [] = ([], []) + go st (Event Open pid l : rest) = + set st pid Top `add` set st pid (Start l) `add` go (set st pid Active) rest + go st (Event Close pid l : rest) = + set st pid (Ret l) `add` set st pid Bottom `add` go (set st pid Deactive) rest + +size :: Cmd -> Int +size Top = 4 +size (Start l) = 6 + length l +size Active = 2 +size Deactive = 0 +size (Ret l) = 4 + length l +size Bottom = 4 + +adjust :: Int -> Cmd -> String +adjust n Top = "┌" ++ replicate (n - 4) '─' ++ "┐" +adjust n (Start l) = "│ " ++ l ++ replicate (n - length l - 6) ' ' ++ " │" +adjust n Active = "│" ++ replicate (n - 4) ' ' ++ "│" +adjust n Deactive = replicate (n - 2) ' ' +adjust n (Ret l) = "│ " ++ replicate (n - 8 - length l) ' ' ++ "⟶ " ++ l ++ " │" +adjust n Bottom = "└" ++ replicate (n - 4) '─' ++ "┘" + +next :: ([Cmd], [Cmd]) -> [String] +next (left, right) = take (length left `max` length right) $ zipWith merge left' right' + where + left' = map (adjust $ maximum $ 0:map size left) (left ++ repeat Deactive) + right' = map (adjust $ maximum $ 0:map size right) (right ++ repeat Deactive) + merge x y = x ++ " │ " ++ y + +toEvent :: [(EventType, Pid)] -> ([String], [String]) -> [Event] +toEvent [] ([], []) = [] +toEvent [] ps = error $ "toEvent: residue inputs: " ++ show ps +toEvent ((e , Pid 1):evT) (x:xs, ys) = Event e (Pid 1) x : toEvent evT (xs, ys) +toEvent ((_e, Pid 1):_evT) ([] , _ys) = error "toEvent: no input from pid 1" +toEvent ((e , Pid 2):evT) (xs , y:ys) = Event e (Pid 2) y : toEvent evT (xs, ys) +toEvent ((_e, Pid 2):_evT) (_xs , []) = error "toEvent: no input from pid 2" +toEvent (e : _) _ = error $ "toEvent: unknown pid " ++ show e + +compilePrefix :: [String] -> [Cmd] +compilePrefix [] = [] +compilePrefix (cmd:res:prefix) = Top : Start cmd : Ret res : Bottom : compilePrefix prefix +compilePrefix [cmd] = error $ "compilePrefix: doesn't have response for cmd: " ++ cmd + +-- | Given a history, and output from processes generate Doc with boxes +exec :: [(EventType, Pid)] -> Fork [String] -> Doc +exec evT (Fork lops pops rops) = vsep $ map text (preBoxes ++ parBoxes) + where + preBoxes = map (adjust $ maximum $ 0:map ((2+) . length) (take 1 parBoxes)) $ compilePrefix pops + parBoxes = next . compile $ toEvent evT (lops, rops) diff --git a/src/Test/StateMachine/Types.hs b/src/Test/StateMachine/Types.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Types.hs @@ -0,0 +1,256 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE IncoherentInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Test.StateMachine.Types +-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Stevan Andjelkovic +-- Stability : provisional +-- Portability : non-portable (GHC extensions) +-- +-- This module contains the main types exposed to the user. The module +-- is perhaps best read indirectly, on a per need basis, via the main +-- module "Test.StateMachine". +-- +----------------------------------------------------------------------------- + +module Test.StateMachine.Types + ( StateMachineModel(..) + , ShowCmd + , showCmd + , Signature + , Response(..) + , SResponse(..) + , Response_ + , GetResponse_ + , HasResponse + , response + , CommandConstraint + , Untyped(..) + , RefPlaceholder + -- * Indexed variant of 'Functor', 'Foldable' and 'Traversable'. + , Ex(..) + , IxFunctor + , ifmap + , IxFoldable + , ifoldMap + , itoList + , iany + , IxTraversable + , itraverse + , ifor + -- * Indexed variants of some 'constraints' package combinators. + , IxForallF + , Ords + , Ords' + , iinstF + -- * Re-export + , (\\) + , type (@@) + , Property + , property + , Proxy(..) + ) where + +import Data.Constraint +import Data.Constraint.Forall +import Data.Kind + (Type) +import Data.Proxy + (Proxy(..)) +import Data.Singletons.Prelude + (type (@@), Apply, ConstSym1, Sing, TyFun) +import Data.Singletons.TH + (DemoteRep, SDecide, SingKind) +import Data.Typeable + (Typeable) +import Test.QuickCheck.Property + (Property, property) + +import Test.StateMachine.Internal.Types.IntRef + +------------------------------------------------------------------------ + +-- | A state machine based model. +data StateMachineModel model cmd = StateMachineModel + { precondition :: forall refs resp. IxForallF Ord refs => + model refs -> cmd refs resp -> Bool + , postcondition :: forall refs resp. IxForallF Ord refs => + model refs -> cmd refs resp -> Response_ refs resp -> Property + , transition :: forall refs resp. IxForallF Ord refs => + model refs -> cmd refs resp -> Response_ refs resp -> model refs + , initialModel :: forall refs. model refs + } + +-- | Given a command, how can we show it? +class ShowCmd (cmd :: Signature ix) where + + -- | How to show a typed command with internal refereces. + showCmd :: forall resp. cmd (ConstSym1 String) resp -> String + +------------------------------------------------------------------------ + +-- | Signatures of commands contain a family of references and a +-- response type. +type Signature ix = (TyFun ix Type -> Type) -> Response ix -> Type + +------------------------------------------------------------------------ + +-- | A response of a command is either of some type or a referece at +-- some index. +data Response ix + = Response Type + | Reference ix + +-- | The singleton type of responses. +data SResponse ix :: Response ix -> Type where + SResponse :: SResponse ix ('Response t) + SReference :: Sing (i :: ix) -> SResponse ix ('Reference i) + +-- | Given a command, what kind of response does it have? +class HasResponse cmd where + + -- | What type of response a typed command has. + response :: cmd refs resp -> SResponse ix resp + +-- | Type-level function that returns a response type. +type family Response_ (refs :: TyFun ix Type -> Type) + (resp :: Response ix) :: Type where + Response_ refs ('Response t) = t + Response_ refs ('Reference i) = refs @@ i + +-- | Type-level function that maybe returns a response. +type family GetResponse_ (resp :: Response ix) :: k where + GetResponse_ ('Response t) = t + GetResponse_ ('Reference i) = () + +------------------------------------------------------------------------ + +-- | The constraints on commands (and their indices) that the +-- 'Test.StateMachine.sequentialProperty' and +-- 'Test.StateMachine.parallelProperty' helpers require. +type CommandConstraint ix cmd = + ( Ord ix + , SDecide ix + , SingKind ix + , DemoteRep ix ~ ix + , ShowCmd cmd + , IxTraversable cmd + , HasResponse cmd + ) + +------------------------------------------------------------------------ + +-- | Untyped commands are command where we hide the response type. This +-- is used in generation of commands. +data Untyped (f :: Signature ix) refs where + Untyped :: ( Show (GetResponse_ resp) + , Typeable (Response_ ConstIntRef resp) + , Typeable resp + ) => f refs resp -> Untyped f refs + +------------------------------------------------------------------------ + +-- | When generating commands it is enough to provide a reference +-- placeholder. +data RefPlaceholder ix :: (TyFun ix k) -> Type + +type instance Apply (RefPlaceholder _) i = Sing i + +------------------------------------------------------------------------ + +-- | Dependent pairs. +data Ex (p :: TyFun a Type -> Type) = forall (x :: a). Ex (Sing x) (p @@ x) + +-- | Predicate transformers. +class IxFunctor (f :: (TyFun ix Type -> Type) -> jx -> Type) where + + -- | Indexed 'fmap'. + ifmap + :: forall p q j. (forall i. Sing (i :: ix) -> p @@ i -> q @@ i) + -> f p j -> f q j + +-- | Foldable for predicate transformers. +class IxFoldable (t :: (TyFun ix Type -> Type) -> jx -> Type) where + + -- | Indexed 'foldMap'. + ifoldMap :: Monoid m => (forall i. Sing (i :: ix) -> p @@ i -> m) -> t p j -> m + + -- | Indexed 'toList'. + itoList :: t p j -> [Ex p] + itoList = ifoldMap (\s px -> [Ex s px]) + + -- | Indexed 'foldr'. + ifoldr :: (forall i. Sing (i :: ix) -> p @@ i -> b -> b) -> b -> t p j -> b + ifoldr f z = foldr (\(Ex i x) -> f i x) z . itoList + + -- | Indexed 'any'. + iany :: (forall i. Sing (i :: ix) -> p @@ i -> Bool) -> t p j -> Bool + iany p = ifoldr (\i x ih -> p i x || ih) False + +-- | Tranversable for predicate transformers. +class (IxFunctor t, IxFoldable t) => + IxTraversable (t :: (TyFun ix Type -> Type) -> jx -> Type) where + + -- | Indexed traverse function. + itraverse + :: Applicative f + => Proxy q + -> (forall x. Sing x -> p @@ x -> f (q @@ x)) + -> t p j + -> f (t q j) + itraverse pq f tp = ifor pq tp f + + -- | Same as above, with arguments flipped. + ifor + :: Applicative f + => Proxy q + -> t p j + -> (forall x. Sing x -> p @@ x -> f (q @@ x)) + -> f (t q j) + ifor pq tp f = itraverse pq f tp + + {-# MINIMAL itraverse | ifor #-} + +------------------------------------------------------------------------ + +class p (f @@ a) => + IxComposeC (p :: k2 -> Constraint) (f :: TyFun k1 k2 -> Type) (a :: k1) + +instance p (f @@ a) => IxComposeC p f a + +-- | Indexed variant of 'ForallF'. +class Forall (IxComposeC p f) => + IxForallF (p :: k2 -> Constraint) (f :: TyFun k1 k2 -> Type) + +instance Forall (IxComposeC p f) => IxForallF p f + +-- | Indexed variant of 'instF'. +iinstF :: forall a p f. Proxy a -> IxForallF p f :- p (f @@ a) +iinstF _ = Sub $ + case inst :: Forall (IxComposeC p f) :- IxComposeC p f a of + Sub Dict -> Dict + +-- | Type alias that is helpful when defining state machine models. +type Ords refs = IxForallF Ord refs :- Ord (refs @@ '()) + +-- | Same as the above. +type Ords' refs i = IxForallF Ord refs :- Ord (refs @@ i) diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,4 @@ +module Main where + +main :: IO () +main = return ()