diff --git a/src/Search/Search.hs b/src/Search/Search.hs
index 8690301ddefe7e94e42bb0264b7de3cc00ad7aaa..448c51a3d9c27c2f8de58fd439bc9d4dd5294a74 100644
--- a/src/Search/Search.hs
+++ b/src/Search/Search.hs
@@ -1,4 +1,7 @@
 {-# LANGUAGE LambdaCase, OverloadedStrings #-}
+{-# LANGUAGE KindSignatures, DataKinds #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Search.Search (driver) where
 
@@ -17,38 +20,53 @@ import System.Exit
 import System.Process
 import System.IO
 import Data.Foldable
+import Data.Function
+
+data Compare = OnlyState | StateAndSyscall
 
 -- | (Syscall, Statehash)
-type Vertex = (Text, Text)
+newtype Vertex (a :: Compare) = Vertex { unVertex :: (Text, Text) }
+
+instance Eq (Vertex 'OnlyState) where
+  (==) = (==) `on` (snd . unVertex)
+
+instance Eq (Vertex 'StateAndSyscall) where
+  (==) = (==) `on` unVertex
+
+instance Ord (Vertex 'OnlyState) where
+  compare = compare `on` (snd . unVertex)
 
-type Graph = Map Vertex (Set Vertex)
+instance Ord (Vertex 'StateAndSyscall) where
+  compare = compare `on` unVertex
+
+type Graph a = Map (Vertex a) (Set (Vertex a))
 
 type DecisionNumber = Int
-type Decision = (Vertex, DecisionNumber)
+type Decision a = (Vertex a, DecisionNumber)
 data DecisionState = Half [Bool] -- Trace
                    | Full
 
-data State = State
-  { graph :: Graph
-  , currentVertex :: Maybe Vertex
-  , decisions :: Map Decision DecisionState
+data State a = State
+  { graph :: Graph a
+  , currentVertex :: Maybe (Vertex a)
+  , decisions :: Map (Decision a) DecisionState
   , curTrace :: [Bool]
   }
 
-addVertex :: (Text, Text ) -> State -> State
-addVertex vert s = s
-  { graph = case currentVertex s of
-      Just old
-        | old == vert -> graph s
-        | otherwise -> M.insertWith S.union old (S.singleton vert) (graph s)
-      Nothing -> graph s
-  , currentVertex = Just vert
-  }
+addVertex :: Ord (Vertex a) => Vertex a -> State a -> State a
+addVertex vert s =
+  s { graph = case currentVertex s of
+        Just old
+          | old == vert -> graph s
+          | otherwise -> M.insertWith S.union old (S.singleton vert) (graph s)
+        Nothing -> graph s
+    , currentVertex = Just vert
+    }
 
 data NextStep = Restart
               | Continue Bool
 
-handleDecision :: DecisionNumber -> [Bool] -> State -> (NextStep, State)
+handleDecision :: Ord (Vertex a) => DecisionNumber -> [Bool] -> State a -> (NextStep, State a)
 handleDecision decision trace s =
   let curSystemState = fromJust (currentVertex s) -- FIXME fromJust
       decisionState = M.lookup (curSystemState, decision) (decisions s)
@@ -57,29 +75,36 @@ handleDecision decision trace s =
     Just (Half _) -> (Continue False, s { decisions = M.insert (curSystemState, decision) Full (decisions s) })
     Just Full -> (Restart, s)
 
-findOpenDecision :: State -> Maybe [Bool]
+findOpenDecision :: State a -> Maybe [Bool]
 findOpenDecision = listToMaybe . mapMaybe isHalf . M.elems . decisions
   where
     isHalf (Half trace) = Just trace
     isHalf _            = Nothing
 
 
-driver :: FilePath -> IO ()
-driver prog = do
-  state <- newIORef (State M.empty (Just ("", "start")) M.empty [])
+
+driver :: FilePath
+       -> Bool -- ^ Identify states on different locations?
+       -> IO ()
+driver prog False = driver' prog (Vertex ("", "start") :: Vertex 'StateAndSyscall)
+driver prog True = driver' prog (Vertex ("", "start") :: Vertex 'OnlyState)
+
+driver' :: Ord (Vertex a) => FilePath -> Vertex a -> IO ()
+driver' prog startVertex = do
+  state <- newIORef (State M.empty (Just startVertex) M.empty [])
   oneProgRun prog state Nothing
 
   forever $ do
-    modifyIORef state $ \s -> s { curTrace = [], currentVertex = Just ("", "start") }
+    modifyIORef state $ \s -> s { curTrace = [], currentVertex = Just startVertex }
     findOpenDecision <$> readIORef state >>= \case
       Nothing    -> do
         s <- readIORef state
         T.putStrLn (graph2Dot (graph s))
         exitSuccess
-      Just trace -> do
+      Just trace ->
         oneProgRun prog state (Just $ reverse trace)
 
-oneProgRun :: FilePath -> IORef State -> Maybe [Bool] -> IO ()
+oneProgRun :: Ord (Vertex a) => FilePath -> IORef (State a) -> Maybe [Bool] -> IO ()
 oneProgRun prog state trace = do
   (Just pstdin, Just pstdout, _, handle) <- createProcess (proc prog []) { std_in = CreatePipe, std_out = CreatePipe }
   case trace of
@@ -93,8 +118,8 @@ oneProgRun prog state trace = do
           writeIORef state s'
           case next of
             Restart -> terminateProcess handle >> mapM_ hClose [pstdin, pstdout]
-            Continue x -> do
-              makeDecision pstdin state x
+            Continue x' -> do
+              makeDecision pstdin state x'
               loop
 
         EOF -> terminateProcess handle >> mapM_ hClose [pstdin, pstdout]
@@ -103,28 +128,28 @@ oneProgRun prog state trace = do
   loop
 
 
-tracePath :: Handle -> Handle -> IORef State -> [Bool] -> IO ()
-tracePath pstdin pstdout state [] = return ()
-tracePath pstdin pstdout state (decision:ds) = do
+tracePath :: Ord (Vertex a) => Handle -> Handle -> IORef (State a) -> [Bool] -> IO ()
+tracePath _ _ _ [] = return ()
+tracePath pstdin pstdout state (decision:ds) =
   handleLine pstdout state >>= \case
     EOF -> error "premature eof" -- FIXME
-    Decision x -> do
+    Decision _ -> do
       makeDecision pstdin state decision
       tracePath pstdin pstdout state ds
     NewState _ -> tracePath pstdin pstdout state (decision:ds)
 
-makeDecision :: Handle -> IORef State -> Bool -> IO ()
+makeDecision :: Handle -> IORef (State a) -> Bool -> IO ()
 makeDecision pstdin state decision = do
   hPutStrLn pstdin $ if decision then "1" else "0"
   hFlush pstdin
   modifyIORef state (\s -> s { curTrace = decision : curTrace s})
   hPutStrLn stderr $ "deciding " ++ show decision
 
-data LineOut = NewState Vertex
-             | Decision DecisionNumber
-             | EOF
+data LineOut a = NewState (Vertex a)
+               | Decision DecisionNumber
+               | EOF
 
-parseLine :: Handle -> IO LineOut
+parseLine :: Handle -> IO (LineOut a)
 parseLine handle = do
   eof <- hIsEOF handle
   if eof
@@ -135,14 +160,14 @@ parseLine handle = do
       case T.words line of
         ("Decision":num:_) -> return $ Decision (read $ T.unpack num)
         ["Line",linum,"before","syscall",call,"in","state",state]
-          -> return $ NewState (call, state)
+          -> return $ NewState $ Vertex (call, state)
 
-handleLine :: Handle -> IORef State -> IO LineOut
+handleLine :: Ord (Vertex a) => Handle -> IORef (State a) -> IO (LineOut a)
 handleLine pstdin state = parseLine pstdin >>= \case
   NewState vert -> modifyIORef state (addVertex vert) >> return (NewState vert)
   other         -> return other
 
-graph2Dot :: Graph -> Text
+graph2Dot :: Ord (Vertex a) => Graph a -> Text
 graph2Dot graph =
      "digraph gcfg {\n"
   <> dotNodes graph
@@ -152,19 +177,19 @@ graph2Dot graph =
   where
     nodeStr from tos = mconcat $ map (arrow from) $ S.toList tos
     arrow from to = "  " <> nodeId from <> " -> "
-      <> nodeId to <> " [label=\"" <> edgeLabel (fst from) <> "\"];\n"
+      <> nodeId to <> " [label=\"" <> edgeLabel (fst $ unVertex from) <> "\"];\n"
     edgeLabel txt = T.dropEnd 1 $ T.dropWhileEnd (/='_') $
       T.drop (T.length "OSEKOS_") txt
 
-dotNodes :: Graph -> Text
+dotNodes :: Ord (Vertex a) => Graph a -> Text
 dotNodes = foldMap formatNode . allNotes
   where
-    allNotes m = M.keysSet m `S.union` (fold m)
-    formatNode (call, state) = nodeId (call,state)
+    allNotes m = M.keysSet m `S.union` fold m
+    formatNode (Vertex (call, state)) = nodeId (Vertex (call,state))
                             <> " [label=\""
                             <> "State: " <> state <> "\\n"
                             <> "Syscall: " <> call
                             <> "\", shape=box];\n"
 
-nodeId :: Vertex -> Text
-nodeId (call, state) = "node" <> state <> "_" <> call
+nodeId :: Vertex a -> Text
+nodeId (Vertex (call, state)) = "node" <> state <> "_" <> call
diff --git a/src/main/Main.hs b/src/main/Main.hs
index 0dc1e3c0676ac2a2a6a3510df719686238e6117b..b7de4402f23ade5c7275142f067c9fa3bc88f272 100644
--- a/src/main/Main.hs
+++ b/src/main/Main.hs
@@ -28,17 +28,22 @@ optParser = subparser
 
 data SearchOpts = SearchOpts
   { mockupExecutable :: FilePath
+  , identifyStates :: Bool
   }
 
 searchOptParser :: Parser SearchOpts
-searchOptParser = SearchOpts <$> argument str (metavar "EXECUTABLE")
+searchOptParser = SearchOpts
+  <$> argument str (metavar "EXECUTABLE")
+  <*> switch ( long "identify-states"
+            <> help "Identify equal states at different source locations"
+             )
 
 main :: IO ()
 main = do
   cmd <- execParser $ info (helper <*> optParser)
             ( fullDesc <> progDesc "dOSEK verification tool" )
   case cmd of
-    (Search opts) -> driver (mockupExecutable opts)
+    (Search opts) -> driver (mockupExecutable opts) (identifyStates opts)
     Mockup        -> do
       cntnt <- BS.getContents
       case P.parseFile cntnt of