Remove 'Killed' thread action

Closes #198

dejafu-tests/lib/Unit/Properties.hs

@@ -78,9 +78,7 @@ commonProps :: [TestTree]
 commonProps = toTestList
   [ testProperty "simplifyAction a == simplifyLookahead (rewind a)" $ do
       act <- H.forAll genThreadAction
-      case D.rewind act of
-        Just lh -> D.simplifyAction act H.=== D.simplifyLookahead lh
-        Nothing -> H.discard
+      D.simplifyAction act H.=== D.simplifyLookahead (D.rewind act)
 
   , testProperty "isBarrier a ==> synchronises a r" $ do
       a <- H.forAll (HGen.filter D.isBarrier genActionType)
@@ -169,19 +167,15 @@ sctProps = toTestList
       ds <- H.forAll genDepState
       tid <- H.forAll genThreadId
       act <- H.forAll (HGen.filter (SCT.canInterrupt ds tid) genThreadAction)
-      case D.rewind act of
-        Just lh -> H.assert (SCT.canInterruptL ds tid lh)
-        Nothing -> H.discard
+      H.assert (SCT.canInterruptL ds tid (D.rewind act))
 
   , testProperty "dependent ==> dependent'" $ do
       ds <- H.forAll genDepState
       tid1 <- H.forAll genThreadId
       tid2 <- H.forAll genThreadId
       ta1 <- H.forAll genThreadAction
       ta2 <- H.forAll (HGen.filter (SCT.dependent ds tid1 ta1 tid2) genThreadAction)
-      case D.rewind ta2 of
-        Just lh -> H.assert (SCT.dependent' ds tid1 ta1 tid2 lh)
-        Nothing -> H.discard
+      H.assert (SCT.dependent' ds tid1 ta1 tid2 (D.rewind ta2))
 
   , testProperty "dependent x y == dependent y x" $ do
       ds <- H.forAll genDepState
@@ -306,7 +300,6 @@ genThreadAction = HGen.choice
   , pure D.Throw
   , D.ThrowTo <$> genThreadId
   , D.BlockedThrowTo <$> genThreadId
-  , pure D.Killed
   , D.SetMasking <$> HGen.bool <*> genMaskingState
   , D.ResetMasking <$> HGen.bool <*> genMaskingState
   , pure D.LiftIO

dejafu/CHANGELOG.rst

@@ -15,6 +15,11 @@ Fixed
 * (:issue:`243`) Add missing dependency for ``setNumCapabilities``
   actions.
 
+Removed
+~~~~~~~
+
+* (:issue:`198`) ``Test.DejaFu.Types.Killed``, which was unused.
+
 
 1.3.0.1 (2018-03-08)
 --------------------

dejafu/Test/DejaFu/Internal.hs

@@ -157,49 +157,48 @@ tvarsRead act = S.fromList $ case act of
 
 -- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has
 -- happened. 'Killed' has no 'Lookahead' counterpart.
-rewind :: ThreadAction -> Maybe Lookahead
-rewind (Fork _) = Just WillFork
-rewind (ForkOS _) = Just WillForkOS
-rewind (IsCurrentThreadBound _) = Just WillIsCurrentThreadBound
-rewind MyThreadId = Just WillMyThreadId
-rewind (GetNumCapabilities _) = Just WillGetNumCapabilities
-rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)
-rewind Yield = Just WillYield
-rewind (ThreadDelay n) = Just (WillThreadDelay n)
-rewind (NewMVar _) = Just WillNewMVar
-rewind (PutMVar c _) = Just (WillPutMVar c)
-rewind (BlockedPutMVar c) = Just (WillPutMVar c)
-rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c)
-rewind (ReadMVar c) = Just (WillReadMVar c)
-rewind (BlockedReadMVar c) = Just (WillReadMVar c)
-rewind (TryReadMVar c _) = Just (WillTryReadMVar c)
-rewind (TakeMVar c _) = Just (WillTakeMVar c)
-rewind (BlockedTakeMVar c) = Just (WillTakeMVar c)
-rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c)
-rewind (NewCRef _) = Just WillNewCRef
-rewind (ReadCRef c) = Just (WillReadCRef c)
-rewind (ReadCRefCas c) = Just (WillReadCRefCas c)
-rewind (ModCRef c) = Just (WillModCRef c)
-rewind (ModCRefCas c) = Just (WillModCRefCas c)
-rewind (WriteCRef c) = Just (WillWriteCRef c)
-rewind (CasCRef c _) = Just (WillCasCRef c)
-rewind (CommitCRef t c) = Just (WillCommitCRef t c)
-rewind (STM _ _) = Just WillSTM
-rewind (BlockedSTM _) = Just WillSTM
-rewind Catching = Just WillCatching
-rewind PopCatching = Just WillPopCatching
-rewind Throw = Just WillThrow
-rewind (ThrowTo t) = Just (WillThrowTo t)
-rewind (BlockedThrowTo t) = Just (WillThrowTo t)
-rewind Killed = Nothing
-rewind (SetMasking b m) = Just (WillSetMasking b m)
-rewind (ResetMasking b m) = Just (WillResetMasking b m)
-rewind LiftIO = Just WillLiftIO
-rewind Return = Just WillReturn
-rewind Stop = Just WillStop
-rewind Subconcurrency = Just WillSubconcurrency
-rewind StopSubconcurrency = Just WillStopSubconcurrency
-rewind (DontCheck _) = Just WillDontCheck
+rewind :: ThreadAction -> Lookahead
+rewind (Fork _) = WillFork
+rewind (ForkOS _) = WillForkOS
+rewind (IsCurrentThreadBound _) = WillIsCurrentThreadBound
+rewind MyThreadId = WillMyThreadId
+rewind (GetNumCapabilities _) = WillGetNumCapabilities
+rewind (SetNumCapabilities i) = WillSetNumCapabilities i
+rewind Yield = WillYield
+rewind (ThreadDelay n) = WillThreadDelay n
+rewind (NewMVar _) = WillNewMVar
+rewind (PutMVar c _) = WillPutMVar c
+rewind (BlockedPutMVar c) = WillPutMVar c
+rewind (TryPutMVar c _ _) = WillTryPutMVar c
+rewind (ReadMVar c) = WillReadMVar c
+rewind (BlockedReadMVar c) = WillReadMVar c
+rewind (TryReadMVar c _) = WillTryReadMVar c
+rewind (TakeMVar c _) = WillTakeMVar c
+rewind (BlockedTakeMVar c) = WillTakeMVar c
+rewind (TryTakeMVar c _ _) = WillTryTakeMVar c
+rewind (NewCRef _) = WillNewCRef
+rewind (ReadCRef c) = WillReadCRef c
+rewind (ReadCRefCas c) = WillReadCRefCas c
+rewind (ModCRef c) = WillModCRef c
+rewind (ModCRefCas c) = WillModCRefCas c
+rewind (WriteCRef c) = WillWriteCRef c
+rewind (CasCRef c _) = WillCasCRef c
+rewind (CommitCRef t c) = WillCommitCRef t c
+rewind (STM _ _) = WillSTM
+rewind (BlockedSTM _) = WillSTM
+rewind Catching = WillCatching
+rewind PopCatching = WillPopCatching
+rewind Throw = WillThrow
+rewind (ThrowTo t) = WillThrowTo t
+rewind (BlockedThrowTo t) = WillThrowTo t
+rewind (SetMasking b m) = WillSetMasking b m
+rewind (ResetMasking b m) = WillResetMasking b m
+rewind LiftIO = WillLiftIO
+rewind Return = WillReturn
+rewind Stop = WillStop
+rewind Subconcurrency = WillSubconcurrency
+rewind StopSubconcurrency = WillStopSubconcurrency
+rewind (DontCheck _) = WillDontCheck
 
 -- | Check if an operation could enable another thread.
 willRelease :: Lookahead -> Bool
@@ -315,7 +314,7 @@ tidsOf _ = S.empty
 -- This is used in the SCT code to help determine interesting
 -- alternative scheduling decisions.
 simplifyAction :: ThreadAction -> ActionType
-simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind
+simplifyAction = simplifyLookahead . rewind
 
 -- | Variant of 'simplifyAction' that takes a 'Lookahead'.
 simplifyLookahead :: Lookahead -> ActionType

dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

@@ -611,9 +611,7 @@ dependent ds t1 a1 t2 a2 = case (a1, a2) of
   (BlockedSTM _, STM _ _)      -> checkSTM
   (BlockedSTM _, BlockedSTM _) -> checkSTM
 
-  _ -> case (,) <$> rewind a1 <*> rewind a2 of
-    Just (l1, l2) -> dependent' ds t1 a1 t2 l2 && dependent' ds t2 a2 t1 l1
-    _ -> dependentActions ds (simplifyAction a1) (simplifyAction a2)
+  _ -> dependent' ds t1 a1 t2 (rewind a2) && dependent' ds t2 a2 t1 (rewind a1)
 
   where
     -- STM actions A and B are dependent if A wrote to anything B

dejafu/Test/DejaFu/Types.hs

@@ -2,7 +2,7 @@
 
 -- |
 -- Module      : Test.DejaFu.Types
--- Copyright   : (c) 2017 Michael Walker
+-- Copyright   : (c) 2017--2018 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -85,7 +85,7 @@ initialThread = ThreadId (Id (Just "main") 0)
 
 -- | All the actions that a thread can perform.
 --
--- @since 1.1.0.0
+-- @since unreleased
 data ThreadAction =
     Fork ThreadId
   -- ^ Start a new thread.
@@ -156,8 +156,6 @@ data ThreadAction =
   -- ^ Throw an exception to a thread.
   | BlockedThrowTo ThreadId
   -- ^ Get blocked on a 'throwTo'.
-  | Killed
-  -- ^ Killed by an uncaught exception.
   | SetMasking Bool MaskingState
   -- ^ Set the masking state. If 'True', this is being used to set the
   -- masking state to the original state in the argument passed to a