content: -- import Debug.QuickCheck
  import Test.QuickCheck
  import System.IO.Unsafe
  import Control.Concurrent.MVar
  import Control.Concurrent
  import Control.Monad
  
  
  data Action = NewEmptyMVar | NewMVar Int | TakeMVar | ReadMVar | PutMVar Int
  	    | SwapMVar Int | IsEmptyMVar | ReturnInt Int | ReturnBool Bool
    deriving (Eq,Show)
  
  main = do 
    t <- myThreadId
    forkIO (threadDelay 20000000 >> killThread t)
  	-- just in case we deadlock
    testMVar
  
  testMVar :: IO ()
  testMVar = do
    quickCheck prop_NewEIs_NewERet
    quickCheck prop_NewIs_NewRet
    quickCheck prop_NewTake_NewRet
    quickCheck prop_NewEPutTake_NewERet
    quickCheck prop_NewRead_NewRet
    quickCheck prop_NewSwap_New
  
  
  prop_NewEIs_NewERet = 
    [NewEmptyMVar,IsEmptyMVar] =^ [NewEmptyMVar,ReturnBool True]
  
  prop_NewIs_NewRet n = 
    [NewMVar n,IsEmptyMVar] =^ [NewMVar n,ReturnBool False]
  
  prop_NewTake_NewRet n =
    [NewMVar n,TakeMVar] =^ [NewEmptyMVar,ReturnInt n]
  
  prop_NewEPutTake_NewERet n = 
    [NewEmptyMVar,PutMVar n,TakeMVar] =^ 
      [NewEmptyMVar,ReturnInt n]
  
  prop_NewRead_NewRet n = 
    [NewMVar n,ReadMVar] =^ [NewMVar n,ReturnInt n]
  
  prop_NewSwap_New m n =
    [NewMVar m,SwapMVar n] =^ [NewMVar n]
  
  
  perform :: [Action] -> IO ([Bool],[Int])
  perform [] = return ([],[])
  
  perform (a:as) =
    case a of
      ReturnInt v	 -> liftM (\(b,l) -> (b,v:l)) (perform as)
      ReturnBool v -> liftM (\(b,l) -> (v:b,l)) (perform as)
      NewEmptyMVar -> newEmptyMVar >>= \mv -> perform' mv as
      NewMVar n    -> newMVar n >>= \mv -> perform' mv as    
      _		 -> error $ "Please use NewMVar or NewEmptyMVar as first "
  			    ++ "action"
  
  
  perform' :: MVar Int -> [Action] -> IO ([Bool],[Int])
  perform' _ [] = return ([],[])
  
  perform' mv (a:as) =
    case a of
      ReturnInt v	 -> liftM (\(b,l) -> (b,v:l)) (perform' mv as)
      ReturnBool v -> liftM (\(b,l) -> (v:b,l)) (perform' mv as)
      TakeMVar     -> liftM2 (\v (b,l) -> (b,v:l)) (takeMVar mv) 
  			        (perform' mv as)
      ReadMVar     -> liftM2 (\v (b,l) -> (b,v:l)) (readMVar mv) 
  			        (perform' mv as)
      PutMVar n    -> putMVar mv n >> perform' mv as
      SwapMVar n	 -> swapMVar mv n >> perform' mv as
      IsEmptyMVar  -> liftM2 (\v (b,l) -> (v:b,l)) (isEmptyMVar mv)
  				(perform' mv as)
      _		 -> error $ "If you want to use " ++ show a 
  			    ++ " please use the =^ operator"
  
  
  actions :: Gen [Action]
  actions = do
    oneof [liftM (NewEmptyMVar:) (actions' True),
  	 liftM2 (:) (liftM NewMVar arbitrary) (actions' False)] 
  
  
  actions' :: Bool -> Gen [Action]
  actions' empty =
    oneof ([return [],
  	  liftM (IsEmptyMVar:) (actions' empty)] ++
  	  if empty
  	     then [liftM2 (:) (liftM PutMVar arbitrary) (actions' False)]
  	     else []
  	  ++
  	  if empty
  	     then []
  	     else [liftM (TakeMVar:) (actions' True)]
  	  ++
  	  if empty
  	     then []
  	     else [liftM (ReadMVar:) (actions' False)]
  	  ++
  	  if empty
  	     then []
  	     else [liftM2 (:) (liftM SwapMVar arbitrary) (actions' False)]   )
  
  
  (=^) :: [Action] -> [Action] -> Property
  c =^ c' =
    forAll (actions' (delta True c))
  	 (\suff -> observe c suff == observe c' suff)
    where observe x suff = unsafePerformIO (perform (x++suff))
  
  
  (^=^) :: [Action] -> [Action] -> Property
  c ^=^ c' =
    forAll actions
  	 (\pref -> forAll (actions' (delta True (pref++c)))
  			  (\suff -> observe c pref suff == 
  				      observe c' pref suff))
    where observe x pref suff = unsafePerformIO (perform (pref++x++suff))
  
  
  delta :: Bool -> [Action] -> Bool
  delta b [] = b
  
  delta b (ReturnInt _:as) = delta b as
  
  delta b (ReturnBool _:as) = delta b as
  
  delta _ (NewEmptyMVar:as) = delta True as
  
  delta _ (NewMVar _:as) = delta False as
  
  delta b (TakeMVar:as) = delta (if b
  				  then error "take on empty MVar"
  				  else True) as
  
  delta b (ReadMVar:as) = delta (if b
  				  then error "read on empty MVar"
  				  else False) as
  
  delta _ (PutMVar _:as) = delta False as
  
  delta b (SwapMVar _:as) = delta (if b
  				  then error "swap on empty MVar"
  				  else False) as
  
  delta b (IsEmptyMVar:as) = delta b as
  