packages feed

quickcheck-state-machine (empty) → 0.0.0

raw patch · 17 files changed

+1910/−0 lines, 17 filesdep +QuickCheckdep +ansi-wl-pprintdep +basesetup-changed

Dependencies added: QuickCheck, ansi-wl-pprint, base, constraints, containers, hspec, mtl, parallel-io, quickcheck-state-machine, random, singletons, stm

Files

+ CHANGELOG.md view
@@ -0,0 +1,3 @@+#### 0.0.0++  * Initial release.
+ LICENSE view
@@ -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.
+ README.md view
@@ -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).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ quickcheck-state-machine.cabal view
@@ -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 <stevan@advancedtelematic.com>+homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme+synopsis: Test monadic programs using state machine based models+description:+    See README at <https://github.com/advancedtelematic/quickcheck-state-machine#readme>+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
+ src/Test/StateMachine.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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
+ src/Test/StateMachine/Internal/AlphaEquality.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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+-- <https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference/Prop.hs metaproperties>.+--+-----------------------------------------------------------------------------++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
+ src/Test/StateMachine/Internal/IxMap.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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)
+ src/Test/StateMachine/Internal/Parallel.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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
+ src/Test/StateMachine/Internal/ScopeCheck.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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+-- <https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference/Prop.hs metaproperties>.+--+-----------------------------------------------------------------------------++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)
+ src/Test/StateMachine/Internal/Sequential.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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
+ src/Test/StateMachine/Internal/Types.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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
+ src/Test/StateMachine/Internal/Types/IntRef.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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
+ src/Test/StateMachine/Internal/Utils.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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 ]
+ src/Test/StateMachine/Internal/Utils/BoxDrawer.hs view
@@ -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 <daniel@advancedtelematic.com>+-- 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)
+ src/Test/StateMachine/Types.hs view
@@ -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 <stevan@advancedtelematic.com>+-- 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)
+ test/Spec.hs view
@@ -0,0 +1,4 @@+module Main where++main :: IO ()+main = return ()