quickcheck-state-machine 0.0.0 → 0.1.0

raw patch · 18 files changed

+1189/−1168 lines, 18 filesdep −constraintsdep −hspecdep −quickcheck-state-machine

Dependencies removed: constraints, hspec, quickcheck-state-machine, singletons

Files

• CHANGELOG.md +6/−0
• LICENSE +1/−1
• README.md +269/−52
• quickcheck-state-machine.cabal +5/−11
• src/Test/StateMachine.hs +120/−79
• src/Test/StateMachine/Internal/AlphaEquality.hs +35/−83
• src/Test/StateMachine/Internal/IxMap.hs +0/−80
• src/Test/StateMachine/Internal/Parallel.hs +188/−245
• src/Test/StateMachine/Internal/ScopeCheck.hs +22/−26
• src/Test/StateMachine/Internal/Sequential.hs +112/−226
• src/Test/StateMachine/Internal/Types.hs +61/−54
• src/Test/StateMachine/Internal/Types/Environment.hs +92/−0
• src/Test/StateMachine/Internal/Types/IntRef.hs +0/−54
• src/Test/StateMachine/Internal/Utils.hs +10/−30
• src/Test/StateMachine/Internal/Utils/BoxDrawer.hs +8/−7
• src/Test/StateMachine/Types.hs +59/−220
• src/Test/StateMachine/Types/HFunctor.hs +56/−0
• src/Test/StateMachine/Types/References.hs +145/−0

@@ -1,3 +1,9 @@+#### 0.1.0++  * The API has been simplified, thanks to ideas stolen+    from+    [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog/commit/385c92f9dd0aa7e748fc677b2eeead5e3572685f).+ #### 0.0.0    * Initial release.

@@ -1,4 +1,4 @@-Copyright Stevan Andjelkovic, Daniel Gustafsson (c) 2017+Copyright (c) 2017 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley  All rights reserved. 

@@ -18,40 +18,227 @@ `quickcheck-state-machine` library can be seen as an attempt to provide similar functionality to Haskell's QuickCheck library. -### Sample run (teaser)+### Example -Here's a sample output from when we look for race conditions in the mutable-reference example:+As a first example, let's implement and test programs using mutable+references. Our implementation will be using `IORef`s, but let's start with a+representation of what actions are possible with program using mutable+references. Our mutable references can be created, read from, written to and+incremented: +```haskell+data Action (v :: * -> *) :: * -> * where+  New   ::                                     Action v (Opaque (IORef Int))+  Read  :: Reference v (Opaque (IORef Int)) -> Action v Int+  Write :: Reference v (Opaque (IORef Int)) -> Int -> Action v ()+  Inc   :: Reference v (Opaque (IORef Int)) -> Action v () ```-> quickCheck (MutableReference.prop_parallel RaceCondition)-*** Failed! (after 5 tests and 6 shrinks): -Couldn't linearise:+When we generate actions we won't be able to create arbitrary `IORef`s, that's+why all uses of `IORefs` are wrapped in `Reference v`, where the parameter `v`+will let us use symbolic references while generating (and concrete ones when+executing). -┌──────────────────────┐-│ New                  │-│                 ⟶ $0 │-└──────────────────────┘-            │ ┌────────┐-            │ │ Inc $0 │-┌─────────┐ │ │        │-│ Inc $0  │ │ │        │-│         │ │ │   ⟶ () │-│         │ │ └────────┘-│    ⟶ () │ │-└─────────┘ │-┌─────────┐ │-│ Read $0 │ │-│     ⟶ 1 │ │-└─────────┘ │+In order to be able to show counterexamples, we need a show instance for our+actions. `IORef`s don't have a show instance, thats why we wrap them in+`Opaque`; which gives a show instance to a type that doesn't have one. +Next, we give the actual implementation of our mutable references. To make+things more interesting, we parametrise the semantics by a possible problem. +```haskell+data Problem = None | Bug | RaceCondition+  deriving Eq++semantics :: Problem -> Action Concrete resp -> IO resp+semantics _   New           = Opaque <$> newIORef 0+semantics _   (Read  ref)   = readIORef  (opaque ref)+semantics prb (Write ref i) = writeIORef (opaque ref) i'+  where+  -- One of the problems is a bug that writes a wrong value to the+  -- reference.+  i' | i `elem` [5..10] = if prb == Bug then i + 1 else i+     | otherwise        = i+semantics prb (Inc   ref)   =+  -- The other problem is that we introduce a possible race condition+  -- when incrementing.+  if prb == RaceCondition+  then do+    i <- readIORef (opaque ref)+    threadDelay =<< randomRIO (0, 5000)+    writeIORef (opaque ref) (i + 1)+  else+    atomicModifyIORef' (opaque ref) (\i -> (i + 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+Note that above `v` is instatiated to `Concrete`, which is essentially the+identity type, so while writing the semantics we have access to real `IORef`s.++We now have an implementation, the next step is to define a model for the+implementation to be tested against. We'll use a simple map between references+and integers as a model.++```haskell+newtype Model v = Model [(Reference v (Opaque (IORef Int)), Int)]++initModel :: Model v+initModel = Model []+```++The pre-condition of an action specifies in what context the action is+well-defined. For example, we can always create a new mutuable reference, but+we can only read from references that already have been created. The+pre-conditions are used while generating programs (lists of actions).++```haskell+precondition :: Model Symbolic -> Action Symbolic resp -> Bool+precondition _         New           = True+precondition (Model m) (Read  ref)   = ref `elem` map fst m+precondition (Model m) (Write ref _) = ref `elem` map fst m+precondition (Model m) (Inc   ref)   = ref `elem` map fst m+```++The transition function explains how actions change the model. Note that the+transition function is polymorphic in `v`. The reason for this is that we use+the transition function both while generating and executing.++```haskell+transition :: Model v -> Action v resp -> v resp -> Model v+transition (Model m) New           ref = Model (m ++ [(Reference ref, 0)])+transition m         (Read  _)     _   = m+transition (Model m) (Write ref i) _   = Model (update ref i         m)+transition (Model m) (Inc   ref)   _   = Model (update ref (old + 1) m)+  where+  Just old = lookup ref m++update :: Eq a => a -> b -> [(a, b)] -> [(a, b)]+update ref i m = (ref, i) : filter ((/= ref) . fst) m+```++Post-conditions are checked after we executed an action and got access to the+result.++```haskell+postcondition :: Model Concrete -> Action Concrete resp -> resp -> Property+postcondition _         New         _    = property True+postcondition (Model m) (Read ref)  resp = lookup ref m === Just resp+postcondition _         (Write _ _) _    = property True+postcondition _         (Inc _)     _    = property True+```++Finally, we have to explain how to generate and shrink actions.++```haskell+generator :: Model Symbolic -> Gen (Untyped Action)+generator (Model m)+  | null m    = pure (Untyped New)+  | otherwise = frequency+      [ (1, pure (Untyped New))+      , (8, Untyped .    Read  <$> elements (map fst m))+      , (8, Untyped <$> (Write <$> elements (map fst m) <*> arbitrary))+      , (8, Untyped .    Inc   <$> elements (map fst m))+      ]++shrinker :: Action v resp -> [Action v resp]+shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]+shrinker _             = []+```++We can now define a sequential property as follows.++```haskell+prop_references :: Problem -> Property+prop_references prb = forAllProgram+  generator+  shrinker+  precondition+  transition+  initModel $ \prog ->+    runAndCheckProgram+      precondition+      transition+      postcondition+      initModel+      (semantics prb)+      ioProperty+      prog+```++If we run the sequential property without introducing any problems to the+semantics function, i.e. `quickCheck (prop_references None)`, then the property+passes. If we however introduce the bug problem, then it will fail with the+minimal counterexample:++```+> quickCheck (prop_references Bug)+*** Failed! Falsifiable (after 16 tests and 4 shrinks):+[New (Var 0),Write (Var 0) 5 (Var 2),Read (Var 0) (Var 3)]+Just 5 /= Just 6+```++Recall that the bug problem causes the write of values ``i `elem` [5..10]`` to+actually write `i + 1`.++Running the sequential property with the race condition problem will not uncover+the race condition.++If we however define a parallel property as follows.++```haskell+prop_referencesParallel :: Problem -> Property+prop_referencesParallel prb = forAllParallelProgram+  generator+  shrinker+  precondition+  transition+  initModel $ \parallel ->+    runParallelProgram (semantics prb) parallel $ \hist ->+      checkParallelProgram+        transition+        postcondition+        initModel+        parallel+        hist+```++And run it using the race condition problem, then we'll find the race+condition:++```+> quickCheck (prop_referencesParallel RaceCondition)+*** Failed! (after 8 tests and 6 shrinks):++Couldn't linearise:++┌────────────────────────────────┐+│ Var 0 ← New                    │+│                       ⟶ Opaque │+└────────────────────────────────┘+┌─────────────┐ │+│ Inc (Var 0) │ │+│             │ │ ┌──────────────┐+│             │ │ │ Inc (Var 0)  │+│        ⟶ () │ │ │              │+└─────────────┘ │ │              │+                │ │         ⟶ () │+                │ └──────────────┘+                │ ┌──────────────┐+                │ │ Read (Var 0) │+                │ │          ⟶ 1 │+                │ └──────────────┘+Just 2 /= Just 1+```++As we can see above, a mutable reference is first created, and then in+parallel (concurrently) we do two increments of said reference, and finally we+read the value `1` while the model expects `2`.++Recall that incrementing is implemented by first reading the reference and+then writing it, if two such actions are interleaved then one of the writes+might end up overwriting the other ones -- creating the 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). @@ -59,31 +246,32 @@  The rought idea is that the user of the library is asked to provide: -  * a datatype of commands;+  * a datatype of actions;   * 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+  * pre- and post-conditions of the actions on the model;+  * a state transition function that given a model and a action advances the     model to its next state;-  * a way to generate and shrink commands;-  * semantics for executing the commands.+  * a way to generate and shrink actions;+  * semantics for executing the actions. -The library then gives back a sequential and a parallel property.+The library then gives back a bunch of combinators that let you define 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;+  1. generate a list of actions; -  2. starting from the initial model, for each command do the the following:+  2. starting from the initial model, for each action do the the following:         1. check that the pre-condition holds;-       2. if so, execute the command using the semantics;+       2. if so, execute the action 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+  3. If something goes wrong, shrink the initial list of actions and present a      minimal counter example.  #### Parallel property@@ -93,28 +281,27 @@ 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+  1. generate a list of actions that will act as a sequential prefix for the      parallel program (think of this as an initialisation bit that setups up      some state); -  2. generate two lists of commands that will act as parallel suffixes;+  2. generate two lists of actions 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;+     invocations and responses of each action; -  5. try to find a possible sequential interleaving of command invocations and+  5. try to find a possible sequential interleaving of action 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+### More examples -To get started it is perhaps easiest to have a look at one of the several-examples:+Here are some more examples to get you started:    * The water jug problem from *Die Hard 2* -- this is a     simple@@ -156,9 +343,11 @@   * 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+    a simple example where the parallel property is used once again to find a+    race condition. The semantics in this example uses a simple database file+    that needs to be setup and teared down. This example also appears 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.@@ -203,20 +392,20 @@     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)+    - [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+        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+        Software Engineering;       - [Abstract State Machines](http://www.di.unipi.it/~boerger/AsmBook/): A-        Method for High-Level System Design and Analysis+        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@@ -230,6 +419,34 @@         *Sequential Abstract State Machines Capture Sequential         Algorithms*         [[PDF](http://delta-apache-vm.cs.tau.ac.il/~nachumd/models/gurevich.pdf)].++  * Other similar libraries:++      - Erlang QuickCheck, [eqc](http://quviq.com/documentation/eqc/), the first+        property based testing library to have support for state machines+        (closed source);++      - The Erlang library [PropEr](https://github.com/manopapad/proper) is+        *eqc*-inspired, open source, and has support for state+        machine [testing](http://propertesting.com/);++      - The Haskell+        library [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog), also+        has support for state machine based testing (no parallel property yet+        though);++      - [ScalaCheck](http://www.scalacheck.org/), likewise has support for state+        machine+        based+        [testing](https://github.com/rickynils/scalacheck/blob/master/doc/UserGuide.md#stateful-testing) (no+        parallel property);++      - The Python+        library [Hypothesis](https://hypothesis.readthedocs.io/en/latest/), also+        has support for state machine+        based+        [testing](https://hypothesis.readthedocs.io/en/latest/stateful.html) (no+        parallel property).  ### License 

@@ -1,5 +1,5 @@ name: quickcheck-state-machine-version: 0.0.0+version: 0.1.0 cabal-version: >=1.10 build-type: Simple license: BSD3@@ -25,25 +25,24 @@     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.Types.Environment         Test.StateMachine.Internal.Utils         Test.StateMachine.Internal.Utils.BoxDrawer         Test.StateMachine.Types+        Test.StateMachine.Types.HFunctor+        Test.StateMachine.Types.References     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@@ -52,12 +51,7 @@     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.*+        base >=4.9.1.0 && <4.10     default-language: Haskell2010     hs-source-dirs: test     ghc-options: -threaded -rtsopts -with-rtsopts=-N

@@ -1,6 +1,5 @@-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Rank2Types            #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE Rank2Types       #-}  ----------------------------------------------------------------------------- -- |@@ -12,108 +11,150 @@ -- Stability   :  provisional -- Portability :  non-portable (GHC extensions) ----- The main module for state machine based testing.+-- The main module for state machine based testing, it contains+-- combinators that help you build sequential and parallel properties. -- -----------------------------------------------------------------------------  module Test.StateMachine-  ( -- * Sequential property helper-    sequentialProperty-  , sequentialProperty'-    -- * Parallel property helper-  , parallelProperty-  , parallelProperty'++  ( -- * Sequential property combinators+    Program+  , forAllProgram+  , runAndCheckProgram+  , runAndCheckProgram'++    -- * Parallel property combinators+  , ParallelProgram+  , forAllParallelProgram+  , History+  , runParallelProgram+  , runParallelProgram'+  , checkParallelProgram++    -- * Types   , module Test.StateMachine.Types   ) where  import           Control.Monad.State-                   (StateT, evalStateT, lift, replicateM_)-import qualified Data.Map                              as M-import           Test.QuickCheck-                   (Gen)+                   (evalStateT, replicateM_) import           Test.QuickCheck.Monadic                    (monadic, monadicIO, run) import           Test.QuickCheck.Property-                   (Property, forAllShrink)+                   (Property, forAllShrink, ioProperty) -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.Types.Environment import           Test.StateMachine.Internal.Utils+                   (liftProperty) 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)+-- | This function is like a 'forAllShrink' for sequential programs.+forAllProgram+  :: Show (Untyped act)+  => HFoldable act+  => Generator model act+  -> Shrinker act+  -> Precondition model act+  -> Transition   model act+  -> InitialModel model+  -> (Program act -> Property)  -- ^ Predicate that should hold for all+                                --   programs.   -> Property-sequentialProperty smm gen shrinker sem runM =-  sequentialProperty' smm (lift gen) () shrinker (const (const sem)) runM+forAllProgram generator shrinker precondition transition model =+  forAllShrink+    (evalStateT (generateProgram generator precondition transition 0) model)+    (shrinkProgram shrinker precondition transition model) --- | 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)+-- | Run a sequential program and check if your model agrees with your+--   semantics.+runAndCheckProgram+  :: Monad m+  => HFunctor act+  => Precondition model act+  -> Transition model act+  -> Postcondition model act+  -> InitialModel model+  -> Semantics act m+  -> (m Property -> Property)  -- ^ Runner+  -> Program act   -> 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+runAndCheckProgram precond trans postcond m sem runner =+  runAndCheckProgram' precond trans postcond m sem (return ()) (const runner) (const (return ())) +-- | Same as above, except with the possibility to setup some resource+--   for the runner to use. The resource could be a database connection+--   for example.+runAndCheckProgram'+  :: Monad m+  => HFunctor act+  => Precondition model act+  -> Transition model act+  -> Postcondition model act+  -> InitialModel model+  -> Semantics act m+  -> IO setup                           -- ^ Setup a resource.+  -> (setup -> m Property -> Property)+  -> (setup -> IO ())                   -- ^ Tear down the resource.+  -> Program act+  -> Property+runAndCheckProgram' precond trans postcond m sem setup runner cleanup acts =+  monadic (ioProperty . runnerWithSetup)+    (checkProgram precond trans postcond m m sem acts)+  where+  runnerWithSetup mp = do+    s <- setup+    let prop = runner s (evalStateT mp emptyEnvironment)+    cleanup s+    return prop+ ------------------------------------------------------------------------ --- | 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+-- | This function is like a 'forAllShrink' for parallel programs.+forAllParallelProgram+  :: Show (Untyped act)+  => HFoldable act+  => Generator model act+  -> Shrinker act+  -> Precondition model act+  -> Transition   model act+  -> InitialModel model+  -> (ParallelProgram act -> Property) -- ^ Predicate that should hold+                                       --   for all parallel programs.   -> Property-parallelProperty smm gen shrinker sem-  = parallelProperty' smm (lift gen) () shrinker sem (return ())+forAllParallelProgram generator shrinker precondition transition model =+  forAllShrink+    (generateParallelProgram generator precondition transition model)+    (shrinkParallelProgram shrinker precondition transition model) -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+-- | Run a parallel program and collect the history of the execution.+runParallelProgram+  :: Show (Untyped act)+  => HTraversable act+  => Semantics act IO+  -> ParallelProgram act+  -> (History act -> Property) -- ^ Predicate that should hold for the+                               --   execution history.   -> 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+runParallelProgram sem = runParallelProgram' (return ()) (const sem) (const (return ()))++-- | Same as above, but with the possibility of setting up some resource.+runParallelProgram'+  :: Show (Untyped act)+  => HTraversable act+  => IO setup                     -- ^ Setup a resource.+  -> (setup -> Semantics act IO)+  -> (setup -> IO ())             -- ^ Tear down the resource.+  -> ParallelProgram act+  -> (History act -> Property)+  -> Property+runParallelProgram' setup sem clean fork checkhistory = monadicIO $ do+  res <- run setup+  replicateM_ 10 $ do+    hist <- run (executeParallelProgram (sem res) fork)+    run (clean res)+    liftProperty (checkhistory hist)

@@ -1,10 +1,4 @@-{-# LANGUAGE DataKinds           #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE PolyKinds           #-}-{-# LANGUAGE Rank2Types          #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeInType          #-}+{-# LANGUAGE FlexibleContexts #-}  ----------------------------------------------------------------------------- -- |@@ -16,7 +10,7 @@ -- Stability   :  provisional -- Portability :  non-portable (GHC extensions) ----- This module provides \(\alpha\)-equality for internal commands. This+-- This module provides \(\alpha\)-equality for internal actions. 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>.@@ -28,92 +22,50 @@   , 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(..))+                   (State, get, modify, evalState, runState)+import           Data.Map+                   (Map)+import qualified Data.Map                    as M -import           Test.StateMachine.Internal.IxMap-                   (IxMap)-import qualified Test.StateMachine.Internal.IxMap as IxM-import           Test.StateMachine.Internal.Types import           Test.StateMachine.Types+import           Test.StateMachine.Internal.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+-- | Check if two lists of actions 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.+  :: (HFunctor act, Eq (Program act))+  => Program act -> Program act     -- ^ The two input programs.   -> Bool-alphaEq c0 c1 = canonical c0 == canonical c1+alphaEq acts1 acts2 = canonical acts1 == canonical acts2 --- | Check if two forks of commands are equal modulo+canonical :: HFunctor act => Program act -> Program act+canonical = Program . fst . flip runState M.empty . canonical' . unProgram++canonical' :: HFunctor act => [Internal act] -> State (Map Var Var) [Internal act]+canonical' []                                   = return []+canonical' (Internal act (Symbolic var) : acts) = do+  env     <- get+  let act' = hfmap (\(Symbolic v) -> Symbolic (env M.! v)) act+      var' = Var (M.size env)+      sym' = Symbolic var'+  modify (M.insert var var')+  ih      <- canonical' acts+  return (Internal act' sym' : ih)++-- | Check if two forks of actions 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.+  :: (HFunctor act, Eq (Program act))+  => Fork (Program act) -> Fork (Program act) -- ^ The two input forks.   -> Bool alphaEqFork f1 f2 = canonicalFork f1 == canonicalFork f2++canonicalFork :: HFunctor act => Fork (Program act) -> Fork (Program act)+canonicalFork (Fork l p r) = Fork (Program l') (Program p') (Program r')+  where+  (p', m) = runState  (canonical' (unProgram p)) M.empty+  l'      = evalState (canonical' (unProgram l)) m+  r'      = evalState (canonical' (unProgram r)) m

@@ -1,80 +0,0 @@-{-# 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)

@@ -1,15 +1,9 @@-{-# LANGUAGE DataKinds                 #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts          #-} {-# LANGUAGE GADTs                     #-} {-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE MultiParamTypeClasses     #-}-{-# LANGUAGE PolyKinds                 #-} {-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE RecordWildCards           #-} {-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TypeInType                #-}-{-# LANGUAGE TypeOperators             #-}  ----------------------------------------------------------------------------- -- |@@ -21,17 +15,17 @@ -- Stability   :  provisional -- Portability :  non-portable (GHC extensions) ----- This module contains the building blocks needed to implement the--- 'Test.StateMachine.parallelProperty' helper.+-- This module contains helpers for generating, shrinking, and checking+-- parallel programs. -- -----------------------------------------------------------------------------  module Test.StateMachine.Internal.Parallel-  ( liftGenFork-  , liftGenFork'-  , liftShrinkFork-  , liftSemFork-  , checkParallelInvariant+  ( generateParallelProgram+  , shrinkParallelProgram+  , executeParallelProgram+  , checkParallelProgram+  , History(..)   ) where  import           Control.Concurrent@@ -45,20 +39,15 @@ import           Control.Monad                    (foldM) import           Control.Monad.State-                   (StateT, evalStateT, execStateT, lift)+                   (StateT, runStateT, evalState, evalStateT, execStateT, get,+                   lift, modify, runState) import           Data.Dynamic-                   (Dynamic, fromDynamic, toDyn)-import           Data.Kind-                   (Type)+                   (Dynamic, toDyn) 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.Set+                   (Set)+import qualified Data.Set                                     as S import           Data.Tree                    (Tree(Node)) import           Data.Typeable@@ -66,149 +55,186 @@ import           System.Random                    (randomRIO) import           Test.QuickCheck-                   (Gen, Property, counterexample, property, (.&&.))-import           Test.QuickCheck.Monadic-                   (PropertyM)+                   (Gen, Property, counterexample, property,+                   shrinkList, (.&&.)) import           Text.PrettyPrint.ANSI.Leijen-                   (Doc, Pretty, pretty, prettyList, text, vsep, (<+>))+                   (Doc) -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.Types.Environment 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) ()+-- | Generate a parallel program whose actions all respect their+--   pre-conditions.+generateParallelProgram+  :: Generator    model act+  -> Precondition model act+  -> Transition   model act+  -> model Symbolic+  -> Gen (ParallelProgram act)+generateParallelProgram generator precondition transition model = do+  let generate     =  generateProgram generator precondition transition+  (prefix, model') <- runStateT  (generate 0) model+  let offset       =  length (unProgram prefix)+  left             <- evalStateT (generate offset) model'+  let offset'      =  offset + length (unProgram left)+  right            <- evalStateT (generate offset') model'+  return (ParallelProgram (Fork left prefix right)) -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)+-- | Shrink a parallel program in a pre-condition and scope respecting+--   way.+shrinkParallelProgram+  :: HFoldable act+  => Shrinker act+  -> Precondition model act+  -> Transition model act+  -> model Symbolic+  -> (ParallelProgram act -> [ParallelProgram act])+shrinkParallelProgram shrinker precondition transition model+  = fmap ParallelProgram+  . go+  . unParallelProgram   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)-  ] +++  go (Fork l p r) = map forkFilterInvalid+    [ Fork l' p' r'+    | (p', (l', r')) <- shrinkPair' shrinker' (shrinkPair shrinker') (p, (l, r))+    ]+    where+    shrinker'+      = map Program+      . shrinkList (liftShrinkInternal shrinker)+      . unProgram -  -- Only shrink the prefix:-  shrinkPrefix f+  forkFilterInvalid (Fork l p r) =+    let+      filterProgram         = filterInvalid precondition transition+      (p', (model', scope)) = runState  (filterProgram p) (model, S.empty)+      l'                    = evalState (filterProgram l) (model', scope)+      r'                    = evalState (filterProgram r) (model', scope)+    in Fork l' p' r' +-- | Run a parallel program, by first executing the prefix sequentially+--   and then the suffixes in parallel, and return the history (or+--   trace) of the execution.+executeParallelProgram+  :: forall act. HTraversable act+  => Show (Untyped act)+  => Semantics act IO+  -> ParallelProgram act+  -> IO (History act)+executeParallelProgram semantics = liftSemFork . unParallelProgram   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)-      ]+  liftSemFork+    :: HTraversable act+    => Show (Untyped act)+    => Fork (Program act)+    -> IO (History act)+  liftSemFork (Fork left prefix right) = do+    hchan <- newTChanIO+    env   <- execStateT (runMany hchan (Pid 0) (unProgram prefix)) emptyEnvironment+    withPool 2 $ \pool ->+      parallel_ pool+        [ evalStateT (runMany hchan (Pid 1) (unProgram left))  env+        , evalStateT (runMany hchan (Pid 2) (unProgram right)) env+        ]+    History <$> getChanContents hchan+    where+    getChanContents :: forall a. TChan a -> IO [a]+    getChanContents chan = reverse <$> atomically (go [])       where-      l'  = removeManyCommands (p : ps) l-      r'  = removeManyCommands (p : ps) r+      go :: [a] -> STM [a]+      go acc = do+        mx <- tryReadTChan chan+        case mx of+          Just x  -> go $ x : acc+          Nothing -> return acc -      l'' = removeCommands p l-      r'' = removeCommands p r+  runMany+    :: HTraversable act+    => Show (Untyped act)+    => TChan (HistoryEvent (UntypedConcrete act))+    -> Pid+    -> [Internal act]+    -> StateT Environment IO ()+  runMany hchan pid = flip foldM () $ \_ (Internal act sym@(Symbolic var)) -> do+    env <- get+    let cact = either (error . show) id (reify env act)+    lift $ atomically $ writeTChan hchan $+      InvocationEvent (UntypedConcrete cact) (show (Untyped act)) var pid+    resp <- lift (semantics cact)+    modify (insertConcrete sym (Concrete resp))+    lift $ do+      threadDelay =<< randomRIO (0, 20)+      atomically $ writeTChan hchan $ ResponseEvent (toDyn resp) (show resp) pid -      removeManyCommands :: [IntRefed cmd] -> [IntRefed cmd] -> [IntRefed cmd]-      removeManyCommands []       ds = ds-      removeManyCommands (c : cs) ds = removeManyCommands cs (removeCommands c ds)+-- | Check if a history from a parallel execution can be linearised.+checkParallelProgram+  :: HFoldable act+  => Transition    model act+  -> Postcondition model act+  -> InitialModel model+  -> ParallelProgram act+  -> History act             -- ^ History to be checked.+  -> Property+checkParallelProgram transition postcondition model prog history+  = counterexample ("Couldn't linearise:\n\n" ++ show (toBoxDrawings allVars history))+  $ linearise transition postcondition model history+  where+  vars xs    = [ getUsedVars x | Internal x _ <- xs]+  Fork l p r = fmap (S.unions . vars . unProgram) $ unParallelProgram prog+  allVars    = S.unions [l, p, r]  ------------------------------------------------------------------------ -type History cmd = [HistoryEvent (IntRefed cmd)]+-- The code below is used by checkParallelProgram. -data HistoryEvent cmd-  = InvocationEvent cmd     Pid-  | ResponseEvent   Dynamic Pid+-- | A history is a trace of invocations and responses from running a+--   parallel program.+newtype History act = History+  { unHistory :: History' act } -getProcessIdEvent :: HistoryEvent cmd -> Pid-getProcessIdEvent (InvocationEvent _ pid) = pid-getProcessIdEvent (ResponseEvent   _ pid) = pid+type History' act = [HistoryEvent (UntypedConcrete act)] -data Operation cmd = forall resp.-  (Show (GetResponse_ resp),-   HasResponse cmd,-   Typeable resp,-   Typeable (Response_ ConstIntRef resp)) =>-  Operation (cmd ConstIntRef resp) (Response_ ConstIntRef resp) Pid+data UntypedConcrete (act :: (* -> *) -> * -> *) where+  UntypedConcrete :: (Show resp, Typeable resp) =>+    act Concrete resp -> UntypedConcrete act -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+data HistoryEvent act+  = InvocationEvent act     String Var Pid+  | ResponseEvent   Dynamic String     Pid -takeInvocations :: History cmd -> [HistoryEvent (IntRefed cmd)]+getProcessIdEvent :: HistoryEvent act -> Pid+getProcessIdEvent (InvocationEvent _ _ _ pid) = pid+getProcessIdEvent (ResponseEvent   _ _ pid)   = pid++data Operation act = forall resp. Typeable resp =>+  Operation (act Concrete resp) String (Concrete resp) Pid++takeInvocations :: [HistoryEvent a] -> [HistoryEvent a] takeInvocations = takeWhile $ \h -> case h of-  InvocationEvent _ _ -> True-  _                   -> False+  InvocationEvent {} -> True+  _                  -> False -findCorrespondingResp :: Pid -> History cmd -> [(Dynamic, History cmd)]+findCorrespondingResp :: Pid -> History' act -> [(Dynamic, History' act)] findCorrespondingResp _   [] = []-findCorrespondingResp pid (ResponseEvent resp pid' : es) | pid == pid' = [(resp, es)]+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 :: History' act -> [Tree (Operation act)] linearTree [] = [] linearTree es =-  [ Node (Operation cmd (dynResp resp) pid) (linearTree es')-  | InvocationEvent (IntRefed cmd _) pid <- takeInvocations es+  [ Node (Operation act str (dynResp resp) pid) (linearTree es')+  | InvocationEvent (UntypedConcrete act) str _ pid <- takeInvocations es   , (resp, es')  <- findCorrespondingResp pid $ filter1 (not . matchInv pid) es   ]   where-  dynResp resp = fromMaybe (error "linearTree: impossible.") (fromDynamic resp)+  dynResp resp = either (error . show) id (reifyDynamic resp)    filter1 :: (a -> Bool) -> [a] -> [a]   filter1 _ []                   = []@@ -216,132 +242,49 @@                      | otherwise = xs    -- Hmm, is this enough?-  matchInv pid (InvocationEvent _ pid') = pid == pid'-  matchInv _   _                        = False+  matchInv pid (InvocationEvent _ _ _ pid') = pid == pid'+  matchInv _   _                            = False  linearise-  :: forall cmd model-  .  HasResponse cmd-  => StateMachineModel model cmd-  -> History cmd+  :: forall model act+  .  Transition    model act+  -> Postcondition model act+  -> InitialModel model+  -> History act   -> Property-linearise _                        [] = property True-linearise StateMachineModel {..} xs0 = anyP (step initialModel) . linearTree $ xs0+linearise transition postcondition model0 = go . unHistory   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+  go :: History' act -> Property+  go [] = property True+  go es = anyP (step model0) (linearTree es)++  step :: model Concrete -> Tree (Operation act) -> Property+  step model (Node (Operation act _ resp@(Concrete resp') _) roses) =+    postcondition model act resp' .&&.+    anyP' (step (transition model act 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)+toBoxDrawings :: Set Var -> History act -> Doc+toBoxDrawings knownVars (History h) = exec evT (fmap out <$> Fork l p r)   where-  (p, h') = partition (\e -> getProcessIdEvent e == 0) h-  (l, r)  = partition (\e -> getProcessIdEvent e == 1) h'+    (p, h') = partition (\e -> getProcessIdEvent e == Pid 0) h+    (l, r)  = partition (\e -> getProcessIdEvent e == Pid 1) h' -  p'      = mkOps p+    out :: HistoryEvent act -> String+    out (InvocationEvent _ str var _)+      | var `S.member` knownVars = show var ++ " ← " ++ str+      | otherwise = str+    out (ResponseEvent _ str _) = str -  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."+    toEventType :: [HistoryEvent act] -> [(EventType, Pid)]+    toEventType = map go+      where+      go e = case e of+        InvocationEvent _ _ _ pid -> (Open,  pid)+        ResponseEvent   _ _   pid -> (Close, pid) -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+    evT = toEventType (filter (\e -> getProcessIdEvent e `elem` map Pid [1,2]) h)

@@ -1,5 +1,3 @@-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE PolyKinds           #-} {-# LANGUAGE Rank2Types          #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -13,7 +11,7 @@ -- Stability   :  provisional -- Portability :  non-portable (GHC extensions) ----- This module provides scope-checking for internal commands. This+-- This module provides scope-checking for internal actions. 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>.@@ -22,35 +20,33 @@  module Test.StateMachine.Internal.ScopeCheck   ( scopeCheck-  , scopeCheckFork+  , scopeCheckParallel   ) where +import           Data.Monoid+                   ((<>))+import           Data.Set+                   (Set)+import qualified Data.Set                              as S++import           Test.StateMachine.Internal.Sequential+                   (getUsedVars) 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 []+-- | Scope-check a program, i.e. make sure that no action uses a+--   reference that doesn't exist.+scopeCheck :: forall act. HFoldable act => Program act -> Bool+scopeCheck = go S.empty . unProgram   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+  go :: Set Var -> [Internal act] -> Bool+  go _     []                                    = True+  go known (Internal act (Symbolic var) : iacts) =+    getUsedVars act `S.isSubsetOf` known && go (S.insert var known) iacts --- | 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)+-- | Same as above, but for parallel programs.+scopeCheckParallel :: HFoldable act => ParallelProgram act -> Bool+scopeCheckParallel (ParallelProgram (Fork l p r)) =+  scopeCheck (p <> l) && scopeCheck (p <> r)

@@ -1,14 +1,6 @@-{-# LANGUAGE DataKinds           #-}-{-# LANGUAGE ExplicitNamespaces  #-} {-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE PolyKinds           #-} {-# LANGUAGE Rank2Types          #-}-{-# LANGUAGE RecordWildCards     #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE TypeInType          #-}-{-# LANGUAGE TypeOperators       #-}  ----------------------------------------------------------------------------- -- |@@ -20,246 +12,140 @@ -- Stability   :  provisional -- Portability :  non-portable (GHC extensions) ----- This module contains the building blocks needed to implement the--- 'Test.StateMachine.sequentialProperty' helper.+-- This module contains helpers for generating, shrinking, and checking+-- sequential programs. -- -----------------------------------------------------------------------------  module Test.StateMachine.Internal.Sequential-  ( liftGen-  , liftGen'-  , liftShrinker-  , liftShrink-  , liftSem-  , removeCommands-  , collectStats-  , checkSequentialInvariant-  ) where+  ( generateProgram+  , filterInvalid+  , getUsedVars+  , liftShrinkInternal+  , shrinkProgram+  , checkProgram+  )+  where +import           Control.Monad+                   (filterM, foldM_) 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+                   (State, StateT, get, lift, modify, put, evalState) 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 qualified Data.Set                                     as S import           Test.QuickCheck-                   (Gen, choose, classify, counterexample, label,-                   sized)+                   (Gen, shrinkList, sized, choose, suchThat) import           Test.QuickCheck.Monadic-                   (PropertyM, monitor, pre, run)-import           Test.QuickCheck.Property-                   (Property)+                   (PropertyM, pre, run) -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.Types.Environment 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+-- | Generate programs whose actions all respect their pre-conditions.+generateProgram+  :: forall model act+  .  Generator    model act+  -> Precondition model act+  -> Transition   model act+  -> Int                     -- ^ Name supply for symbolic variables.+  -> StateT (model Symbolic) Gen (Program act)+generateProgram generator precondition transition index = do+  size <- lift (sized (\k -> choose (0, k)))+  Program <$> go size index   where-  go []       = []-  go (c : cs) =-    [ [] ] ++-    [ removeCommands c cs ] ++-    [ c' : cs' | (c', cs') <- shrinkPair (liftShrinker shrinker) go (c, cs) ]+  go :: Int -> Int -> StateT (model Symbolic) Gen [Internal act]+  go 0  _  = return []+  go sz ix = do+    model <- get+    Untyped act <- lift (generator model `suchThat`+      \(Untyped act) -> precondition model act)+    let sym = Symbolic (Var ix)+    put (transition model act sym)+    acts <- go (sz - 1) (ix + 1)+    return (Internal act sym : acts) --- | 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)+-- | Filter out invalid actions from a program. An action is invalid if+--   either its pre-condition doesn't hold, or it uses references that+--   are not in scope.+filterInvalid+  :: HFoldable act+  => Precondition model act+  -> Transition   model act+  -> Program act+  -> State (model Symbolic, Set Var) (Program act) -- ^ Where @Set Var@+                                                   --   is the scope.+filterInvalid precondition transition+  = fmap Program+  . filterM go+  . unProgram   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+  go (Internal act sym@(Symbolic var)) = do+    (model, scope) <- get+    put (transition model act sym, S.insert var scope)+    return (precondition model act && getUsedVars act `S.isSubsetOf` scope) -  env <- get-  let cmd' = ifmap @_ @_ @_ @_ @refs (\s i -> env IxM.! (s, i)) cmd+-- | Returns the set of references an action uses.+getUsedVars :: HFoldable act => act Symbolic a -> Set Var+getUsedVars = hfoldMap (\(Symbolic v) -> S.singleton v) -  case response cmd' of-    SResponse    -> lift $ sem cmd'-    SReference i -> do-      ref <- lift $ sem cmd'-      modify $ IxM.insert i iref ref-      return iref+-- | Given a shrinker of typed actions we can lift it to a shrinker of+--   internal actions.+liftShrinkInternal :: Shrinker act -> (Internal act -> [Internal act])+liftShrinkInternal shrinker (Internal act sym) =+  [ Internal act' sym | act' <- shrinker act ] -------------------------------------------------------------------------+-- | Shrink a program in a pre-condition and scope respecting way.+shrinkProgram+  :: HFoldable act+  => Shrinker  act+  -> Precondition model act+  -> Transition   model act+  -> model Symbolic+  ->  Program act             -- ^ Program to shrink.+  -> [Program act]+shrinkProgram shrinker precondition transition model+  = map ( flip evalState (model, S.empty)+        . filterInvalid precondition transition+        . Program+        )+  . shrinkList (liftShrinkInternal shrinker)+  . unProgram --- | 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"+-- | For each action in a program, check that if the pre-condition holds+--   for the action, then so does the post-condition.+checkProgram+  :: Monad m+  => HFunctor act+  => Precondition  model act+  -> Transition    model act+  -> Postcondition model act+  -> model Symbolic  -- ^ The model with symbolic references is used to+                     -- check pre-conditions against.+  -> model Concrete  -- ^ While the one with concrete referenes is used+                     -- for checking post-conditions.+  -> Semantics act m+  -> Program   act+  -> PropertyM (StateT Environment m) ()+checkProgram precondition transition postcondition smodel0 cmodel0 semantics+  = foldM_ go (smodel0, cmodel0)+  . unProgram   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+  go (smodel, cmodel) (Internal act sym) = do+    pre (precondition smodel act)+    env <- run get+    let cact = hfmap (fromSymbolic env) act+    resp <- run (lift (semantics cact))+    liftProperty (postcondition cmodel cact resp)+    let cresp = Concrete resp+    run (modify (insertConcrete sym cresp))+    return (transition smodel act sym, transition cmodel cact cresp)+    where+    fromSymbolic :: Environment -> Symbolic v ->  Concrete v+    fromSymbolic env sym' = case reifyEnvironment env sym' of+      Left  err -> error (show err)+      Right con -> con

@@ -1,12 +1,7 @@-{-# LANGUAGE DataKinds            #-} {-# LANGUAGE DeriveFunctor        #-}-{-# LANGUAGE ExplicitNamespaces   #-} {-# LANGUAGE FlexibleContexts     #-} {-# LANGUAGE GADTs                #-}-{-# LANGUAGE PolyKinds            #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeInType           #-}-{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE KindSignatures       #-} {-# LANGUAGE UndecidableInstances #-}  -----------------------------------------------------------------------------@@ -24,71 +19,83 @@ -----------------------------------------------------------------------------  module Test.StateMachine.Internal.Types-  ( IntRef(..)+  ( Program(..)+  , ParallelProgram(..)   , Pid(..)-  , Ref(..)-  , ConstIntRef-  , IntRefed(..)   , Fork(..)-  , showResponse_-  , MayResponse_+  , Internal(..)   ) where -import           Data.Kind-                   (Type)-import           Data.Monoid-                   ((<>))-import           Data.Singletons.Prelude-                   (type (@@), TyFun)+import           Data.List+                   (intercalate) import           Data.Typeable                    (Typeable)-import           Text.PrettyPrint.ANSI.Leijen-                   (Pretty, align, dot, indent, int, pretty, text,-                   underline, vsep, (<+>))+import           Text.Read+                   (readListPrec, readListPrecDefault, readPrec) -import           Test.StateMachine.Internal.Types.IntRef import           Test.StateMachine.Types+                   (Untyped(Untyped))+import           Test.StateMachine.Types.HFunctor+import           Test.StateMachine.Types.References  ------------------------------------------------------------------------ --- | 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+-- | A (sequential) program is an abstract datatype representing a list+--   of actions.+--+-- The idea is that the user shows how to generate, shrink, execute and+-- modelcheck individual actions, and then the below combinators lift+-- those things to whole programs.+newtype Program act = Program { unProgram :: [Internal act] } --- | 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 Eq (Internal act) => Eq (Program act) where+  Program acts1 == Program acts2 = acts1 == acts2 -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 ++ ")"+instance Monoid (Program act) where+  mempty                                = Program []+  Program acts1 `mappend` Program acts2 = Program (acts1 ++ acts2) --- | 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).+instance (Show (Untyped act), HFoldable act) => Show (Program act) where+  show (Program iacts) = bracket . intercalate "," . map go $ iacts+    where++    go (Internal act (Symbolic var)) =+      show (Untyped act) ++ " " ++ show var++    bracket s = "[" ++ s ++ "]"++instance Read (Internal act) => Read (Program act) where+  readPrec     = Program <$> readPrec+  readListPrec = readListPrecDefault++------------------------------------------------------------------------++-- | A parallel program is an abstract datatype that represents three+--   sequences of actions; a sequential prefix and two parallel+--   suffixes. Analogous to the sequential case, the user shows how to+--   generate, shrink, execute and modelcheck individual actions, and+--   then the below combinators lift those things to whole parallel+--   programs.+newtype ParallelProgram act = ParallelProgram+  { unParallelProgram :: Fork (Program act) }++instance (Show (Untyped act), HFoldable act) => Show (ParallelProgram act) where+  show = show . unParallelProgram++-- | Forks are used to represent parallel programs. 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)-    ]+------------------------------------------------------------------------ +-- | An internal action is an action together with the symbolic variable+--   that will hold its result.+data Internal (act :: (* -> *) -> * -> *) where+  Internal :: (Show resp, Typeable resp) =>+    act Symbolic resp -> Symbolic resp -> Internal act+ ------------------------------------------------------------------------ --- | Show function for 'Response_'.-showResponse_-  :: Show (GetResponse_ resp)-  => SResponse ix resp -> Response_ ConstIntRef resp -> String-showResponse_ SResponse      = show-showResponse_ (SReference _) = showRef+-- | A process id.+newtype Pid = Pid Int+  deriving (Eq, Show)

@@ -0,0 +1,92 @@+{-# LANGUAGE Rank2Types          #-}+{-# LANGUAGE ScopedTypeVariables #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Test.StateMachine.Internal.Types.Environment+-- Copyright   :  (C) 2017, Jacob Stanley+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability   :  provisional+-- Portability :  non-portable (GHC extensions)+--+-- This module contains environments that are used to translate between symbolic+-- and concrete references. It's taken verbatim from the Hedgehog+-- <https://hackage.haskell.org/package/hedgehog library>.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Internal.Types.Environment+  ( Environment(..)+  , EnvironmentError(..)+  , emptyEnvironment+  , insertConcrete+  , reifyDynamic+  , reifyEnvironment+  , reify+  ) where++import           Data.Dynamic+                   (Dynamic, Proxy(Proxy), TypeRep, Typeable,+                   dynTypeRep, fromDynamic, toDyn, typeRep)+import           Data.Map+                   (Map)+import qualified Data.Map                as M++import           Test.StateMachine.Types++------------------------------------------------------------------------++-- | A mapping of symbolic values to concrete values.+--+newtype Environment =+  Environment {+      unEnvironment :: Map Var Dynamic+    } deriving (Show)++-- | Environment errors.+--+data EnvironmentError =+    EnvironmentValueNotFound !Var+  | EnvironmentTypeError !TypeRep !TypeRep+    deriving (Eq, Ord, Show)++-- | Create an empty environment.+--+emptyEnvironment :: Environment+emptyEnvironment =+  Environment M.empty++-- | Insert a symbolic / concrete pairing in to the environment.+--+insertConcrete :: Symbolic a -> Concrete a -> Environment -> Environment+insertConcrete (Symbolic k) (Concrete v) =+  Environment . M.insert k (toDyn v) . unEnvironment++-- | Cast a 'Dynamic' in to a concrete value.+--+reifyDynamic :: forall a. Typeable a => Dynamic -> Either EnvironmentError (Concrete a)+reifyDynamic dyn =+  case fromDynamic dyn of+    Nothing ->+      Left $ EnvironmentTypeError (typeRep (Proxy :: Proxy a)) (dynTypeRep dyn)+    Just x ->+      Right $ Concrete x++-- | Turns an environment in to a function for looking up a concrete value from+--   a symbolic one.+--+reifyEnvironment :: Environment -> (forall a. Symbolic a -> Either EnvironmentError (Concrete a))+reifyEnvironment (Environment vars) (Symbolic n) =+  case M.lookup n vars of+    Nothing ->+      Left $ EnvironmentValueNotFound n+    Just dyn ->+      reifyDynamic dyn++-- | Convert a symbolic structure to a concrete one, using the provided environment.+--+reify :: HTraversable t => Environment -> t Symbolic b -> Either EnvironmentError (t Concrete b)+reify vars =+  htraverse (reifyEnvironment vars)

@@ -1,54 +0,0 @@-{-# 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

@@ -1,12 +1,3 @@-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE MultiParamTypeClasses     #-}-{-# LANGUAGE PolyKinds                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE TypeInType                #-}-{-# LANGUAGE TypeOperators             #-}- ----------------------------------------------------------------------------- -- | -- Module      :  Test.StateMachine.Internal.Utils@@ -23,21 +14,17 @@ -----------------------------------------------------------------------------  module Test.StateMachine.Internal.Utils-  ( Shrinker-  , genFromMaybe-  , anyP+  ( anyP   , liftProperty   , shrinkPropertyHelper   , shrinkPropertyHelper'   , shrinkPair+  , shrinkPair'   ) where -import           Control.Monad.State-                   (StateT) import           Test.QuickCheck-                   (Gen, Property, Result(Failure), chatty,-                   counterexample, output, property,-                   quickCheckWithResult, stdArgs)+                   (Property, Result(Failure), chatty, counterexample,+                   output, property, quickCheckWithResult, stdArgs) import           Test.QuickCheck.Monadic                    (PropertyM(MkPropertyM), monadicIO, run) import           Test.QuickCheck.Property@@ -45,17 +32,6 @@  ------------------------------------------------------------------------ --- | 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)@@ -79,7 +55,11 @@     _                                -> 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) =+shrinkPair' :: (a -> [a]) -> (b -> [b]) -> ((a, b) -> [(a, b)])+shrinkPair' shrinkerA shrinkerB (x, y) =   [ (x', y) | x' <- shrinkerA x ] ++   [ (x, y') | y' <- shrinkerB y ]++-- | Same above, but for homogeneous pairs.+shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)])+shrinkPair shrinker = shrinkPair' shrinker shrinker

@@ -8,24 +8,25 @@ -- Stability   :  provisional -- Portability :  non-portable (GHC extensions) ----- This module contains functions for drawing the history for the--- 'Test.StateMachine.parallelProperty'.+-- This module contains functions for visualing a history of a parallel+-- execution. -- -----------------------------------------------------------------------------  module Test.StateMachine.Internal.Utils.BoxDrawer   ( EventType(..)-  , exec)-  where+  , exec+  ) where  import           Text.PrettyPrint.ANSI.Leijen                    (Doc, text, vsep)  import           Test.StateMachine.Internal.Types-                   (Fork(Fork))-import           Test.StateMachine.Internal.Types.IntRef-                   (Pid(..))+                   (Fork(Fork), Pid(..)) +------------------------------------------------------------------------++-- | Event invocation or response. data EventType = Open | Close   deriving (Show) 

@@ -1,20 +1,6 @@-{-# 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   #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE KindSignatures       #-}+{-# LANGUAGE Rank2Types           #-}  ----------------------------------------------------------------------------- -- |@@ -33,224 +19,77 @@ -----------------------------------------------------------------------------  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+  ( -- * Untyped actions+    Untyped(..) --- | Type-level function that maybe returns a response.-type family GetResponse_ (resp :: Response ix) :: k where-  GetResponse_ ('Response  t) = t-  GetResponse_ ('Reference i) = ()+    -- * Type aliases+  , Generator+  , Shrinker+  , Precondition+  , Transition+  , Semantics+  , Postcondition+  , InitialModel -------------------------------------------------------------------------+  -- * Higher-order functors, foldables and traversables+  , module Test.StateMachine.Types.HFunctor --- | 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+  -- * Referenses+  , module Test.StateMachine.Types.References   )------------------------------------------------------------------------------ | 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--------------------------------------------------------------------------+  where --- | When generating commands it is enough to provide a reference---   placeholder.-data RefPlaceholder ix :: (TyFun ix k) -> Type+import           Data.Functor.Classes+                   (Ord1)+import           Data.Typeable+                   (Typeable)+import           Test.QuickCheck+                   (Gen, Property) -type instance Apply (RefPlaceholder _) i = Sing i+import           Test.StateMachine.Types.HFunctor+import           Test.StateMachine.Types.References  ------------------------------------------------------------------------ --- | 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 #-}+-- | An untyped action is an action where the response type is hidden+--   away using an existential type.+--+--   We need to hide the response type when generating actions, because+--   in general the actions we want to generate will have different+--   response types; and thus we can only type the generating function+--   if we hide the response type.+data Untyped (act :: (* -> *) -> * -> *) where+  Untyped :: (Show resp, Typeable resp) => act Symbolic resp -> Untyped act  ------------------------------------------------------------------------ -class p (f @@ a) =>-  IxComposeC (p :: k2 -> Constraint) (f :: TyFun k1 k2 -> Type) (a :: k1)+-- | When generating actions we have access to a model containing+--   symbolic references.+type Generator model act = model Symbolic -> Gen (Untyped act) -instance p (f @@ a) => IxComposeC p f a+-- | Shrinking should preserve the response type of the action.+type Shrinker act = forall (v :: * -> *) resp.+  act v resp -> [act v resp] --- | Indexed variant of 'ForallF'.-class Forall (IxComposeC p f) =>-  IxForallF (p :: k2 -> Constraint) (f :: TyFun k1 k2 -> Type)+-- | Pre-conditions are checked while generating, at this stage we do+--   not yet have access to concrete references.+type Precondition model act = forall resp.+  model Symbolic -> act Symbolic resp -> Bool -instance Forall (IxComposeC p f) => IxForallF p f+-- | The transition function must be polymorphic in the type of+--   variables used, as it is used both while generating and executing.+type Transition model act = forall resp v. Ord1 v =>+  model v -> act v resp -> v resp -> model v --- | 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+-- | When we execute our actions we have access to concrete references.+type Semantics act m = forall resp. act Concrete resp -> m resp --- | Type alias that is helpful when defining state machine models.-type Ords refs = IxForallF Ord refs :- Ord (refs @@ '())+-- | Post-conditions are checked after the actions have been executed+--   and we got a response.+type Postcondition model act = forall resp.+  model Concrete -> act Concrete resp -> resp -> Property --- | Same as the above.-type Ords' refs i = IxForallF Ord refs :- Ord (refs @@ i)+-- | The initial model is polymorphic in the type of references it uses,+--   so that it can be used both in the pre- and the post-condition+--   check.+type InitialModel m = forall (v :: * -> *). m v

@@ -0,0 +1,56 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE KindSignatures    #-}+{-# LANGUAGE Rank2Types        #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Test.StateMachine.Types.HFunctor+-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH, Jacob Stanley+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability   :  provisional+-- Portability :  non-portable (GHC extensions)+--+-- This module exports a higher-order version of functors, foldable functors,+-- and traversable functors.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Types.HFunctor+  ( HFunctor+  , hfmap+  , HFoldable+  , hfoldMap+  , HTraversable+  , htraverse+  )+  where++import           Control.Monad.Identity+                   (Identity(..), runIdentity)+import           Data.Functor.Const+                   (Const(..))++------------------------------------------------------------------------++-- | Higher-order functors.+class HFunctor (f :: (* -> *) -> * -> *) where+  -- | Higher-order version of 'fmap'.+  hfmap :: (forall a. g a -> h a) -> f g b -> f h b++  default hfmap :: HTraversable f => (forall a. g a -> h a) -> f g b -> f h b+  hfmap f = runIdentity . htraverse (Identity . f)++-- | Higher-order foldable functors.+class HFunctor t => HFoldable (t :: (* -> *) -> * -> *) where+  -- | Higher-order version of 'foldMap'.+  hfoldMap :: Monoid m => (forall a. v a -> m) -> t v b -> m++  default hfoldMap :: (HTraversable t, Monoid m) => (forall a. v a -> m) -> t v b -> m+  hfoldMap f = getConst . htraverse (Const . f)++-- | Higher-order traversable functors.+class (HFunctor t, HFoldable t) => HTraversable (t :: (* -> *) -> * -> *) where+  -- | Higher-order version of 'traverse'.+  htraverse :: Applicative f => (forall a. g a -> f (h a)) -> t g b -> f (t h b)

@@ -0,0 +1,145 @@+{-# LANGUAGE DeriveFoldable             #-}+{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveTraversable          #-}+{-# LANGUAGE GADTs                      #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE StandaloneDeriving         #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Test.StateMachine.Types.References+-- Copyright   :  (C) 2017, Jacob Stanley+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability   :  provisional+-- Portability :  non-portable (GHC extensions)+--+-- This module contains reference related types. It's taken almost verbatim from+-- the Hedgehog <https://hackage.haskell.org/package/hedgehog library>.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Types.References+  ( Reference(..)+  , concrete+  , opaque+  , Opaque(..)+  , Symbolic(..)+  , Concrete(..)+  , Var(..)+  ) where++import           Data.Functor.Classes+                   (Eq1(..), Ord1(..), Show1(..), compare1, eq1,+                   showsPrec1)+import           Data.Typeable+                   (Typeable)+import           Text.Read+                   (readPrec)++import           Test.StateMachine.Types.HFunctor++------------------------------------------------------------------------++-- | References are the potential or actual result of executing an action. They+--   are parameterised by either `Symbolic` or `Concrete` depending on the+--   phase of the test.+--+--   `Symbolic` variables are the potential results of actions. These are used+--   when generating the sequence of actions to execute. They allow actions+--   which occur later in the sequence to make use of the result of an action+--   which came earlier in the sequence.+--+--   `Concrete` variables are the actual results of actions. These are used+--   during test execution. They provide access to the actual runtime value of+--   a variable.+--+data Reference v a = Reference (v a)++-- | Take the value from a concrete variable.+--+concrete :: Reference Concrete a -> a+concrete (Reference (Concrete x)) = x++-- | Take the value from an opaque concrete variable.+--+opaque :: Reference Concrete (Opaque a) -> a+opaque (Reference (Concrete (Opaque x))) = x++instance (Eq1 v, Eq a) => Eq (Reference v a) where+  (==) (Reference x) (Reference y) = eq1 x y++instance (Ord1 v, Ord a) => Ord (Reference v a) where+  compare (Reference x) (Reference y) = compare1 x y++instance (Show a, Show1 v) => Show (Reference v a) where+  showsPrec p (Reference x) =+    showParen (p >= 11) $+      showsPrec1 11 x++instance HTraversable Reference where+  htraverse f (Reference v) = fmap Reference (f v)++instance HFunctor  Reference+instance HFoldable Reference++------------------------------------------------------------------------++-- | Opaque values.+--+--   Useful if you want to put something without a 'Show' instance inside+--   something which you'd like to be able to display.+--+newtype Opaque a = Opaque+  { unOpaque :: a+  } deriving (Eq, Ord)++instance Show (Opaque a) where+  showsPrec _ (Opaque _) = showString "Opaque"++-- | Symbolic variable names.+--+newtype Var = Var Int+  deriving (Eq, Ord, Show, Num, Read)++-- | Symbolic values.+--+data Symbolic a where+  Symbolic :: Typeable a => Var -> Symbolic a++deriving instance Eq  (Symbolic a)+deriving instance Ord (Symbolic a)++instance Show (Symbolic a) where+  showsPrec p (Symbolic x) = showsPrec p x++instance Show1 Symbolic where+  liftShowsPrec _ _ p (Symbolic x) = showsPrec p x++instance Typeable a => Read (Symbolic a) where+  readPrec = Symbolic <$> readPrec++instance Eq1 Symbolic where+  liftEq _ (Symbolic x) (Symbolic y) = x == y++instance Ord1 Symbolic where+  liftCompare _ (Symbolic x) (Symbolic y) = compare x y++-- | Concrete values.+--+newtype Concrete a where+  Concrete :: a -> Concrete a+  deriving (Eq, Ord, Functor, Foldable, Traversable)++instance Show a => Show (Concrete a) where+  showsPrec = showsPrec1++instance Show1 Concrete where+  liftShowsPrec sp _ p (Concrete x) = sp p x++instance Eq1 Concrete where+  liftEq eq (Concrete x) (Concrete y) = eq x y++instance Ord1 Concrete where+  liftCompare comp (Concrete x) (Concrete y) = comp x y