fixup! Abstract state machine testing

hedgehog-example/hedgehog-example.cabal

@@ -54,4 +54,4 @@ test-suite test
     , resourcet                       >= 1.1        && < 1.2
     , temporary-resourcet             >= 0.1        && < 0.2
     , text                            >= 1.1        && < 1.3
-    , transformers                    >= 0.3        && < 0.6
+    , transformers                    >= 0.5        && < 0.6

hedgehog-example/test/Test/Example/Registry.hs

@@ -12,7 +12,11 @@ import           Data.Foldable (traverse_)
 import qualified Data.HashTable.IO as HashTable
 import           Data.IORef (IORef)
 import qualified Data.IORef as IORef
+import           Data.Map (Map)
+import qualified Data.Map.Strict as Map
 import           Data.Maybe (isJust, isNothing)
+import           Data.Set (Set)
+import qualified Data.Set as Set
 
 import           Hedgehog
 import qualified Hedgehog.Gen as Gen
@@ -34,17 +38,17 @@ data Pid v =
 
 data Name =
   Name String
-  deriving (Eq, Show)
+  deriving (Eq, Ord, Show)
 
 data State v =
   State {
-      statePids :: [Pid v]
-    , stateRegs :: [(Name, Pid v)]
+      statePids :: Set (Pid v)
+    , stateRegs :: Map Name (Pid v)
     } deriving (Eq, Show)
 
 initialState :: State v
 initialState =
-  State [] []
+  State Set.empty Map.empty
 
 --
 -- FIXME derive automatically, this isn't fun :(
@@ -54,6 +58,10 @@ instance Eq1 v => Eq (Pid v) where
   (==) (Pid x) (Pid y) =
     eq1 x y
 
+instance Ord1 v => Ord (Pid v) where
+  compare (Pid x) (Pid y) =
+    compare1 x y
+
 instance Show1 v => Show (Pid v) where
   showsPrec p (Pid x) =
     showParen (p >= 11) $
@@ -99,7 +107,7 @@ spawn =
         Update $ \s _i o ->
           s {
             statePids =
-              statePids s ++ [Pid o]
+              Set.insert (Pid o) (statePids s)
           }
       ]
 
@@ -142,7 +150,7 @@ register :: Monad m => Command m IO State
 register =
   let
     gen s =
-      case statePids s of
+      case Set.toList (statePids s) of
         [] ->
           Nothing
         xs ->
@@ -156,15 +164,15 @@ register =
   in
     Command gen execute [
         Require $ \s (Register name _) ->
-          notElem name (fmap fst $ stateRegs s)
+          Map.notMember name (stateRegs s)
 
       , Require $ \s (Register _ pid) ->
-          notElem pid (fmap snd $ stateRegs s)
+          notElem pid $ Map.elems (stateRegs s)
 
       , Update $ \s (Register name pid) _o ->
           s {
             stateRegs =
-              stateRegs s ++ [(name, pid)]
+              Map.insert name pid (stateRegs s)
           }
       ]
 
@@ -204,12 +212,12 @@ unregister =
   in
     Command gen execute [
         Require $ \s (Unregister name) ->
-          elem name (fmap fst $ stateRegs s)
+          Map.member name (stateRegs s)
 
       , Update $ \s (Unregister name) _o ->
           s {
             stateRegs =
-              filter ((/= name) . fst) (stateRegs s)
+              Map.delete name (stateRegs s)
           }
       ]
 

hedgehog/hedgehog.cabal

@@ -65,7 +65,7 @@ library
     , text                            >= 1.1        && < 1.3
     , th-lift                         >= 0.7        && < 0.8
     , time                            >= 1.4        && < 1.9
-    , transformers                    >= 0.3        && < 0.6
+    , transformers                    >= 0.5        && < 0.6
     , transformers-base               >= 0.4        && < 0.5
     , wl-pprint-annotated             >= 0.0        && < 0.2
 

hedgehog/src/Hedgehog.hs

@@ -115,11 +115,14 @@ module Hedgehog (
   , Eq1
   , eq1
 
+  , Ord1
+  , compare1
+
   , Show1
   , showsPrec1
   ) where
 
-import           Data.Functor.Classes (Eq1, eq1, Show1, showsPrec1)
+import           Data.Functor.Classes (Eq1, eq1, Ord1, compare1, Show1, showsPrec1)
 
 import           Hedgehog.Internal.Distributive (Distributive(..))
 import           Hedgehog.Internal.Gen (Gen)

hedgehog/src/Hedgehog/Internal/State.hs

@@ -194,7 +194,7 @@ data Callback input output m state =
   --   it must work over 'Symbolic' values when we are generating actions, and
   --   'Concrete' values when we are executing them.
   --
-  | Update (forall v. Eq1 v => state v -> input v -> v output -> state v)
+  | Update (forall v. Ord1 v => state v -> input v -> v output -> state v)
 
   -- | A post-condition for a command that must be verified for the command to
   --   be considered a success.
@@ -215,7 +215,7 @@ callbackRequire1 s i = \case
     True
 
 callbackUpdate1 ::
-     Eq1 v
+     Ord1 v
   => state v
   -> input v
   -> v output
@@ -253,7 +253,7 @@ callbackRequire callbacks s i =
   all (callbackRequire1 s i) callbacks
 
 callbackUpdate ::
-     Eq1 v
+     Ord1 v
   => [Callback input output m state]
   -> state v
   -> input v
@@ -325,7 +325,7 @@ data Action m (state :: (* -> *) -> *) =
         state Symbolic -> input Symbolic -> Bool
 
     , actionUpdate ::
-        forall v. Eq1 v => state v -> input v -> v output -> state v
+        forall v. Ord1 v => state v -> input v -> v output -> state v
 
     , actionEnsure ::
         state Concrete -> input Concrete -> output -> Test m ()