lazy-search 0.1.0.0 → 0.1.1.0

raw patch · 3 files changed

+176/−104 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• lazy-search.cabal +12/−4
• src/Control/Search.hs +96/−93
• src/Data/Coolean.hs +68/−7

@@ -2,9 +2,16 @@ -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                lazy-search
-version:             0.1.0.0
+version:             0.1.1.0
 synopsis:            Finds values satisfying a lazy predicate
--- description:         
+description:         
+  This library can be used as a property based testing driver, and more
+  generally to find values satisfying a predicate (@a -> Bool@). This 
+  is done by a size bounded search, and it uses the laziness of the 
+  predicate to speed up the search by avoiding isomorphic values. 
+  .
+  This is similar to "LazySmallCheck" but uses size instead of depth 
+  and a faster algorithm. 
 license:             BSD3
 license-file:        LICENSE
 author:              Jonas Duregard
@@ -19,6 +26,7 @@   exposed-modules:     Data.Coolean, Control.Search
   -- other-modules:       
   -- other-extensions:    
-  build-depends:       base >=4.8 && <4.9, size-based >=0.1 && <0.2
+  build-depends:       base >=4.7 && <5, size-based >=0.1 && <0.2
   hs-source-dirs:      src
-  default-language:    Haskell2010+  default-language:    Haskell2010
+  -- ghc-options:   -Wall

@@ -1,19 +1,22 @@ {-#LANGUAGE GADTs, DeriveDataTypeable, DeriveFunctor #-}
 
--- | Efficient size-based search for values satisfying/falsifying a lazy boolean predicate. See "Control.Enumerable" for defining enumerations of data types. 
+-- | Efficient size-based search for values satisfying/falsifying a lazy boolean predicate. 
+-- Predicates are typically of type @a -> Bool@, although an alternative boolean type called 'Cool' is provided and using it may give faster searches. 
+--
+-- See "Control.Enumerable" for defining default enumerations of data types (required for searching). 
 module Control.Search 
   ( 
   -- * Searching 
-  search, sat, searchRaw, usearch
+  search, sat, ctrex, searchRaw, usearch
   -- * Testing properties
   , test, testTime
   -- * Options for parallel conjunction
   , Options (..)
-  , sat', search', searchRaw', test'
+  , sat', search', ctrex', searchRaw', test', testTime'
   -- * Deep embedded boolean type
+  , (&&&), (|||), (==>), nott, true, false 
   , Cool(..)
   , Coolean
-  , (&&&), (|||), (==>), nott, true, false 
   -- * Re-exported
   , module Control.Enumerable
   ) where
@@ -22,23 +25,16 @@ import Control.Sized
 import Control.Enumerable
 
-import Data.Bits
 import System.IO.Unsafe
 
 import Control.Enumerable.Count
-import Control.Enumerable.Values
 
-import Data.List ( partition )
 
 import Data.Coolean
 
 import System.Timeout
 
-import Data.List ( nub, (\\) ) -- Just for testing
-import Data.List ( minimumBy ) -- Just for testing
--- import Test.QuickCheck (quickCheck)
 
-
 newCounter :: IO (IO Int)
 newCounter = do
   ref <- newIORef 0
@@ -127,7 +123,7 @@   aconcat []      = empty
   aconcat [s]     = s
   aconcat [s1,s2] = s1 <|> s2
-  aconcat ss = case extr ss of
+  aconcat ss0 = case extr ss0 of
         ([],m)      -> maybe Empty Value m
         (ss',m)     -> maybe (pay (aconcat ss')) (Value . (`mkAlt` (aconcat ss'))) m
       where
@@ -138,6 +134,7 @@         Pay s'    -> case extr ss of
           (ss',Nothing) -> (s':ss',Nothing)
           (ss',j)       -> (s:ss', j)
+      extr _                 = error "internal error"
 
 
 data Observed a = Observed { sizeLeft :: Int, val :: Value a } deriving Functor
@@ -163,11 +160,12 @@      swapped    :: Observed a
   }
 
+(<<) :: Relevant a -> Relevant b -> Bool
 r << q = evalOrder r < evalOrder q
 
 merge :: Value a -> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a,b)]
-merge va vb [] r = rsmap (mkPair va) r
-merge va vb r [] = rsmap (`mkPair` vb) r
+merge va _  [] r = rsmap (mkPair va) r
+merge _  vb r [] = rsmap (`mkPair` vb) r
 merge va vb rs@(r:rs') qs@(q:qs') 
       | q << r     = rmap (va `mkPair`) q : merge va (fixed q) rs  qs'
       | otherwise  = rmap (`mkPair` vb) r : merge (fixed r) vb rs' qs
@@ -175,8 +173,9 @@ -- Alter a Relevant choice by altering both the swapped and fixed value
 rmap :: (Value a -> Value b) -> Relevant a -> Relevant b
 rmap f r = r{fixed = f (fixed r), swapped = omap f (swapped r)} where
-  omap f o' = o'{val = f (val o')}
+  omap g o' = o'{val = g (val o')}
 
+rsmap :: (Value a -> Value b) -> [Relevant a] -> [Relevant b]
 rsmap f = map (rmap f)
 
 
@@ -245,57 +244,57 @@ 
 
 -- Sequential search
-{-#INLINE stepQ #-}
-stepQ :: (a -> Bool) -> State a -> IO ((Bool, a), State a)
-stepQ q ((o:os):s) = do
+{-#INLINE stepD #-}
+stepD :: (a -> Bool) -> State a -> IO ((Bool, a), State a)
+stepD q ((o:os):s) = do
   let s' = if null os then s else os:s  -- Pick a value from the stack
   (ins, a) <- observed o                -- Get an observable copy
   let b = q a
   () <- b `seq` return ()
   os' <- ins                            -- Swap all choices
   return ((b, plainV (val o)), if null os' then s' else os':s')
-stepQ q s             = error $ "Invalid state"
+stepD _ _             = error $ "Invalid state"
 
 
-searchRawQ :: Enumerable a => Int -> (a -> Bool) -> IO [(Bool,a)]
-searchRawQ n q = do
+searchRawD :: Enumerable a => Int -> (a -> Bool) -> IO [(Bool,a)]
+searchRawD n q = do
   let mo = minimal local n
   maybe (return []) (\o -> lazy q [[o]]) mo
   where
     lazy :: (a -> Bool) -> State a -> IO [(Bool,a)]
-    lazy q [] = return []
-    lazy q s = do
-      (ba,s') <- stepQ q s
-      fmap (ba:) (unsafeInterleaveIO $ lazy q s')
+    lazy _ [] = return []
+    lazy q' s = do
+      (ba,s') <- stepD q' s
+      fmap (ba:) (unsafeInterleaveIO $ lazy q' s')
 
 -- Fair Parallel conjunction
-stepP :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
-stepP q ((sc,(o:os)):s) = do
+stepF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
+stepF q ((sc,(o:os)):s) = do
   let s' = if null os then s else (sc,os):s  -- Pick a value from the stack
   (ins, a) <- observed o                     -- Get an observable copy
   let (sc',b) = par sc (q a)
   () <- b `seq` return ()
   os' <- ins                                 -- Swap all choices
   return ((b, plainV (val o)), if null os' then s' else ((sc',os'):s'))
-stepP q s             = error $ "Invalid state"
+stepF _ _             = error $ "Invalid state"
 
 
-searchRawP :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
-searchRawP n q = do
+searchRawF :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
+searchRawF n q = do
   let mo = minimal local n
-  maybe (return []) (\o -> lazyP q [(sched0, [o])]) mo
+  maybe (return []) (\o -> lazy q [(sched0, [o])]) mo
   where 
-    lazyP :: (a -> Cool) -> StateP a -> IO [(Bool,a)]
-    lazyP q [] = return []
-    lazyP q s = do
-      (ba,s') <- stepP q s
-      fmap (ba:) (unsafeInterleaveIO $ lazyP q s')
+    lazy :: (a -> Cool) -> StateP a -> IO [(Bool,a)]
+    lazy _ [] = return []
+    lazy q' s = do
+      (ba,s') <- stepF q' s
+      fmap (ba:) (unsafeInterleaveIO $ lazy q' s')
 
 
 
 -- Short-circuiting sequential search
-stepS :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
-stepS q ((sc,(o:os)):s) = do
+stepO :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
+stepO q ((sc,(o:os)):s) = do
   let s' = if null os then s else (sc,os):s  -- Pick a value from the stack
   
   let (sc', _) = lookahead sc (q (plainV (val o)))
@@ -306,17 +305,17 @@   () <- b `seq` return ()
   os' <- ins                                 -- Swap all choices
   return ((b, plainV (val o)), if null os' then s' else ((sc',os'):s'))
-stepS q s             = error $ "Invalid state"
+stepO _ _             = error $ "Invalid state"
 
-searchRawS :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
-searchRawS n q = do
+searchRawO :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
+searchRawO n q = do
   let mo = minimal local n
   maybe (return []) (\o -> lazy [(sched0, [o])]) mo
   where
     -- lazy :: StateP a -> IO [(Bool,a)]
     lazy [] = return []
     lazy s = do
-      (ba,s') <- stepS q s
+      (ba,s') <- stepO q s
       fmap (ba:) (unsafeInterleaveIO $ lazy s')
 
 
@@ -324,8 +323,8 @@ 
 
 -- Short-circuiting parallel search
-stepSP :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
-stepSP q ((sc,(o:os)):s) = do
+stepOF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
+stepOF q ((sc,(o:os)):s) = do
   let s' = if null os then s else (sc,os):s  -- Pick a value from the stack
   
   let (sc', _) = lookahead sc (q (plainV (val o)))
@@ -334,25 +333,25 @@   () <- b `seq` return ()
   os' <- ins                                 -- Swap all choices
   return ((b, plainV (val o)), if null os' then s' else ((sc'',os'):s'))
-stepSP q s             = error $ "Invalid state"
+stepOF _ _             = error $ "Invalid state"
 
-searchRawSP :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
-searchRawSP n q = do
+searchRawOF :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
+searchRawOF n q = do
   let mo = minimal local n
   maybe (return []) (\o -> lazy [(sched0, [o])]) mo
   where
     -- lazy :: StateP a -> IO [(Bool,a)]
     lazy [] = return []
     lazy s = do
-      (ba,s') <- stepSP q s
+      (ba,s') <- stepOF q s
       fmap (ba:) (unsafeInterleaveIO $ lazy s')
 
 -- Subset-minimize
-stepT :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
-stepT q ((sc,(o:os)):s) = do
+stepOS :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
+stepOS q ((sc,(o:os)):s) = do
   let s' = if null os then s else (sc,os):s  -- Pick a value from the stack
   
-  (c,ins, a1) <- observedc o                 -- Get an observable copy
+  (c,_, a1) <- observedc o                 -- Get an observable copy
   (sc', _) <- subsetsc c sc (q a1)
   
   (ins, a) <- observed o                     -- Get an observable copy
@@ -361,29 +360,27 @@   () <- b `seq` return ()
   os' <- ins                                 -- Swap all choices
   return ((b, plainV (val o)), if null os' then s' else ((sc',os'):s'))
-  
-  
-stepT q s             = error $ "Invalid state"
+stepOS _ _             = error $ "Invalid state"
 
-searchRawT :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
-searchRawT n q = do
+searchRawOS :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
+searchRawOS n q = do
   let mo = minimal local n
   maybe (return []) (\o -> lazy [(sched0, [o])]) mo
   where
     lazy [] = return []
     lazy s = do
-      (ba,s') <- stepT q s
+      (ba,s') <- stepOS q s
       fmap (ba:) (unsafeInterleaveIO $ lazy s')
 
 
--- T + parallel
-stepTP :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
-stepTP q ((sc,(o:os)):s) = do
+-- OS + parallel
+stepOSF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
+stepOSF q ((sc,(o:os)):s) = do
   let s' = if null os then s else (sc,os):s  -- Pick a value from the stack
   
   
-  (c,ins, a1) <- observedc o                 -- Get an observable copy
-  (sc', _) <- subsetsc c sc (q a1)
+  (c,_, a1) <- observedc o                 -- Get an observable copy
+  (sc', _)  <- subsetsc c sc (q a1)
   
   (ins, a) <- observed o                     -- Get an observable copy
   let (sc'',b) = par sc' (q a)
@@ -391,16 +388,16 @@   () <- b `seq` return ()
   os' <- ins                                 -- Swap all choices
   return ((b, plainV (val o)), if null os' then s' else ((sc'',os'):s'))
-stepTP q s             = error $ "Invalid state"
+stepOSF _ _             = error $ "Invalid state"
 
-searchRawTP :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
-searchRawTP n q = do
+searchRawOSF :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
+searchRawOSF n q = do
   let mo = minimal local n
   maybe (return []) (\o -> lazy [(sched0, [o])]) mo
   where
     lazy [] = return []
     lazy s = do
-      (ba,s') <- stepTP q s
+      (ba,s') <- stepOSF q s
       fmap (ba:) (unsafeInterleaveIO $ lazy s')
 
 
@@ -431,7 +428,8 @@       fmap (ba:) (unsafeInterleaveIO $ lazy s')
 -}
 
--- | Options for parallel conjunction strategies
+-- | Options for parallel conjunction strategies. Only matters for 
+-- predicates using the @Cool@ data type instead of Bool.
 data Options 
   = 
     -- | Sequential
@@ -448,22 +446,24 @@   | OSF
   deriving (Show, Read, Eq, Enum)
 
+defOptions :: Coolean cool => (a -> cool) -> Options
 defOptions p | isCool p = OF
-defOptions p            = D
+defOptions _            = D
 
--- | Lazily finds all values isomorphic to p (w.r.t. laziness) and returns them along with the result of p. 
+-- | Lazily finds all non-isomorphic (w.r.t. laziness) inputs to a 
+-- predicate and returns them along with the result of the predicate. 
 searchRaw :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [(Bool,a)]
 searchRaw n p = searchRaw' (defOptions p) n p
 
 searchRaw' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [(Bool,a)]
-searchRaw' D   n p = searchRawQ  n (toBool . p)
-searchRaw' O   n p = searchRawS  n (toCool . p)
-searchRaw' F   n p = searchRawP  n (toCool . p)
-searchRaw' OF  n p = searchRawSP n (toCool . p)
-searchRaw' OS  n p = searchRawT  n (toCool . p)
-searchRaw' OSF  n p = searchRawTP n (toCool . p)
+searchRaw' D   n p = searchRawD  n (toBool . p)
+searchRaw' O   n p = searchRawO  n (toCool . p)
+searchRaw' F   n p = searchRawF  n (toCool . p)
+searchRaw' OF  n p = searchRawOF n (toCool . p)
+searchRaw' OS  n p = searchRawOS  n (toCool . p)
+searchRaw' OSF  n p = searchRawOSF n (toCool . p)
 
--- | Lazily finds all values of or below a given size that satisfies this predicate. 
+-- | Lazily finds all (non-isomorphic) values of or below a given size that satisfy a predicate. 
 search :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [a]
 search n p = search' (defOptions p) n p
 
@@ -479,34 +479,35 @@ sat' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> Bool
 sat' o n q = unsafePerformIO (fmap (not . null) (search' o n q))
 
--- | Unsafe search, the order in which values are found is non-deterministic for some predicates. 
+-- | Unsafe version of search. Non-deterministic for some predicates. 
 usearch :: Enumerable a => Int -> (a -> Bool) -> [a]
 usearch n p = usearch' (defOptions p) n p
 
 usearch' :: Enumerable a => Options -> Int -> (a -> Bool) -> [a]
 usearch' o n q = unsafePerformIO (search' o n q)
 
--- sat' :: Enumerable a => Int -> (a -> Bool) -> Bool
--- sat' n q = unsafePerformIO (fmap (not . null) (search' n q))
 
-
+-- | Find a counterexample to the given predicate, of or below a given size. 
+-- If no counterexample is found, the number of performed executions of the predicate is returned. 
+ctrex :: (Coolean cool, Enumerable a) => Int -> (a -> cool) -> IO (Either Integer a)
+ctrex n p = ctrex' (defOptions p) n p
 
 ctrex' :: (Coolean cool, Enumerable a) => Options -> Int -> (a -> cool) -> IO (Either Integer a)
-ctrex' o n q0 = do 
+ctrex' o n0 q0 = do 
   let q = nott . q0
-  xs <- searchRaw' o n q
+  xs <- searchRaw' o n0 q
   return (go xs 0)
   where go []           n      = Left n
-        go ((b,a):_)    n | b  = Right a
+        go ((b,a):_)    _ | b  = Right a
         go (_    :xs')  n      = go xs' (n+1)
  
 -- Count the domain of a function
 countdom :: Enumerable a => (a -> b) -> Count a
-countdom f = global
+countdom _ = global
 
 test' :: (Coolean cool, Enumerable a, Show a) => Options -> (a -> cool) -> IO ()
 test' o q = go 0 0 (count (countdom q)) where
-  go n _   []     = putStrLn "No counterexample found"
+  go _ _   []     = putStrLn "No counterexample found"
   go n acc (c:cs) = do
     let acc' = acc + c 
     putStrLn $ "Testing to size "++ show n ++ ", worst case "++show acc'++" tests" 
@@ -516,20 +517,23 @@                     go (n+1) acc' cs
       Right x  -> putStrLn "Counterexample found:" >> print x
 
--- | SmallCheck-like test driver. Tests a property with gradually increasing sizes until a conunterexample is found.
+-- | SmallCheck-like test driver. Tests a property with gradually increasing sizes until a conunterexample is found. For each size, it shows the worst case number of tests required 
+-- (if the predicate is fully eager).
 test :: (Coolean cool, Enumerable a, Show a) => (a -> cool) -> IO ()
 test p = test' (defOptions p) p
 
 
 -- | Stop testing after a given number of seconds
 testTime :: (Coolean cool, Enumerable a, Show a) => Int -> (a -> cool) -> IO ()
-testTime t p = do
-  mu <- timeout (t*1000000) (test p)
-  case mu of Nothing -> putStrLn "Timed out"
-             Just x  -> return ()
+testTime t p = testTime' (defOptions p) t p
   
-
+testTime' :: (Coolean cool, Enumerable a, Show a) => Options -> Int -> (a -> cool) -> IO ()
+testTime' o t p = do
+  mu <- timeout (t*1000000) (test' o p)
+  case mu of Nothing  -> putStrLn "Timed out"
+             Just{}   -> return ()
 
+{-
 testall :: (Coolean cool, Enumerable a, Show a) => Options -> (a -> cool) -> IO ()
 testall o q = go 0 0 (count (countdom q)) where
   go n _   []     = putStrLn "No counterexample found"
@@ -542,7 +546,6 @@ 
 
 
-{-
 -- Testing framework
 data Pred where 
   Pred :: (Enumerable a, Show a) => (a -> Cool) -> Pred
@@ -565,7 +568,7 @@ 
 testN' :: (Show a, Enumerable a) => Int -> (a -> Cool) -> IO (Maybe String)
 testN' n p = do
-  xs <- search' SP n p
+  xs <- search' OF n p
   case xs of
     []    -> return Nothing
     (x:_) -> return (Just (show x))

@@ -1,6 +1,17 @@ 
 -- | Proper documentation is TBD
-module Data.Coolean  where
+module Data.Coolean
+ ( Cool(..)
+ -- * Overloaded parallel operators
+ , Coolean(..)
+ , true, false, nott
+ , (&&&), (|||), (==>)
+ -- * Overloaded sequential operators
+ , (!&&), (!||), (!=>)
+ -- * Consumers
+ , Sched(..), sched0
+ , run, lookahead, par, subsetsc
+ ) where
 
 import Control.Exception
 import Data.IORef
@@ -17,36 +28,46 @@           deriving Show
 
 -- Class based construction
-true, false :: Cool
+true :: Cool
 true = Atom True
-false = Atom False
 
+false :: Cool
+false = Atom False
 
+-- | Commutative conjunction
 (&&&) :: (Coolean a, Coolean b) => a -> b -> Cool
 a &&& b = toCool a <&> toCool b
 
-infixr 2 &&&
+infixr 3 &&&
 
+-- | Commutative disjunction
 (|||) :: (Coolean a, Coolean b) => a -> b -> Cool
 a ||| b = toCool a <||> toCool b
 
+infixr 2 |||
+
+-- | Negation
 nott :: Coolean a => a -> Cool
 nott a = Not (toCool a)
 
+-- | Parallel implication
 (==>) :: (Coolean a, Coolean b) => a -> b -> Cool
 a ==> b = Not (toCool a <&> Not (toCool b))
 
--- Sequential operators
-(!=>) :: (Coolean a, Coolean b) => a -> b -> Cool
-a !=> b = Not (toCool a `Seq` Not (toCool b))
 
+-- | Sequential conjunction. Does not evaluate second operand unless first is True. 
 (!&&) :: (Coolean a, Coolean b) => a -> b -> Cool
 a !&& b = toCool a `Seq` toCool b
 
+-- | Sequential disjunction. Does not evaluate second operand unless first is True. 
 (!||) :: (Coolean a, Coolean b) => a -> b -> Cool
 a !|| b = Not (Not (toCool a) `Seq` Not (toCool b))
 
+-- | Sequential implication. Does not evaluate second operand unless first is True. 
+(!=>) :: (Coolean a, Coolean b) => a -> b -> Cool
+a !=> b = Not (toCool a `Seq` Not (toCool b))
 
+
 -- | Provides better interoperability between Bool and Cool by overloading operators. 
 class Coolean b where
   toCool :: b -> Cool
@@ -216,6 +237,46 @@ 
 -- measure :: IO Int -> Sched -> Cool
 
+
+
+{-
+suspending :: IORef (Map ThreadId (ThreadId, ThreadId)) -> IORef (Map ThreadId Integer) -> Cool -> IO Bool
+suspending threads ref c0 = do 
+  mv <- newEmptyMVar
+  forkIO (go (putMVar mv) c0)
+  takeMVar mv
+  
+  where
+  go :: (Bool -> IO ()) -> Cool -> IO ()
+  go res c = case c of
+    Not c'     -> go (res . not) c'
+    And c1 c2  -> do
+      mv <- newEmptyMVar 
+      let res' = putMVar mv
+      t <- myThreadId
+      t1 <- forkIO (go res' c1)
+      t2 <- forkIO (go res' c2)
+      atomicModifyIORef threads (\m -> (M.insert t (t1,t2) m,()))
+      b1 <- takeMVar mv
+      let cleanup = do 
+            ts <- fmap (`clean` (t1,t2)) (readIORef threads)
+            mapM killThread ts
+          ret b = cleanup >> res b
+      case b1 of 
+        False  -> ret False
+        True   -> do
+          b2 <- takeMVar mv
+          case b2 of 
+            False  -> ret False
+            True   -> ret True
+    Atom b     -> evaluate b >>= res
+
+
+clean :: Map ThreadId (ThreadId, ThreadId) -> (ThreadId, ThreadId) -> [ThreadId]
+clean m (t1,t2) = t1:t2:(r t1 ++ r t2)
+  where r t = maybe [] id (fmap (clean m) (M.lookup t m))
+
+-}
 {-
 
 runInterl :: Cool -> Bool